I realized I made two errors in the post above. I want to correct the first and most important with Dafny: my initial introduction to Dafny exercises/examples was:
https://github.com/microsoft/IroncladI found its content full of promise but hard extremely hard to follow: it's hard to see where examples, the libraries, and Dafny itself start or stop ... TLA+ is better documented through slides, PDFs, and Practical TLA+ ebooks etc. The
official repo for
Dafny is,
https://github.com/dafny-lang/dafnyAnd that
does seem well organized. I do not want to throw a wet blanket on people's hard work so I thought I'd better make the distinction clear. I will get back to Dafny as time permits.
>Frama-C or similar is indicated for the CD part of CDCI.
Should have written CI, not CD.
Now returning to the main line of questioning about formal methods in CD/CI ... resistance primarily arises from line programmers. But consider: if I call a team meeting and say that, because we're onboarding a new client, we're putting aside our current work switching to 8 business quarters of new work over 15 JIRA Epics in two week sprints ... well, that's real work ... but nobody is going to stress out too much. After all the work is coming in as JIRA epics which are broken down into smaller stories. As professionals we know Agile is about communication and risk-reduction. Some of the features may not ultimately be needed, and some requirements may change. Attempting the work without that scaffolding would probably not be street smart. Programmers are OK here with some level of lack of complete certainty.
Now contrast: I tell the same team we're doing 8 quarters of other new work with JIRA/Epics but we're going to do formal modeling. Even through formal modeling is also about first order risk reduction ... the complaints will fly: isn't it a waste of time? the code can diverge from the spec at any time? A verified spec says nothing about the what the code does! Are we going to formally verify all the third party libraries we use too? Is that even possible? Here, line programmers suddenly become OCD about perfect predictability and the ease or feasibility with which one can refine down from the spec (JIRA "requirements") into the production code. Suddenly the comfort zone about uncertainty is real. If we can't check it all, we're not even gonna try anything! This, when it happens, is a cultural issue more than technical and it needs leadership to keep things in balance. That's why I say to me formal methods are about primary risk identification and reduction with the same ends as JIRA but different subject matter and means.
Finally, a one-off aside: People have used services and techniques from
https://aphyr.com/ (I am not associated with, talked to, or have every used them) to help debug distributed services. You may find some of that useful, again, in the area of project risk.