But IMO the most useful formal method in Software Engineering is modeling your code as an FSMs, for example using StateCharts UML notation [2,3].
That way even junior developers can reason about complex realtime systems.
Next close come Algebraic Type Systems, but they're usually not available in mainstream PLs.
Unfortunately Formal Specification/Verification tools like TLA+, Alloy, etc. are less practical for most real life projects.
They're a static type systems based on algebraic data types.
The typical argument against Formal Methods is based on cost, to which the reply could be "Well what's the cost of broken code?"
I'm glad the tools and languages to do FM are getting more common and familiar.
Verification is definitely a big concern for junior developers who don't know how to write good tests, however, beyond a certain level of expertise, the big challenge becomes validation.
If written properly, tests do a pretty good job at verification. Formal proofs only take care of rare edge cases (since tests can never be exhaustive), but many times, it's possible (and recommended) to write code in a way to minimize such rare edge cases anyway.
It's all about bang-for-buck: a formal proof can give me lots of confidence about some aspect of a system, but might take a long time and have a maintenance burden; if that time and maintenance could give me more confidence when used to write masses of tests instead, then it's probably better to go with the tests.
My go-to approach is property-based testing, since that can exercise edge-cases more effectively than hand-picked examples, whilst taking about the same amount of effort to write.
A couple of things in favour of "proper" formal methods (in niche circumstances):
- Sometimes the effort calculation tips in favour of a formal methods; e.g. reliably testing concurrent, distributed systems is notoriously hard, and might require even more effort than doing some proofs instead.
- Proof objects themselves, and the act of writing them, can be useful for understanding a domain or system, and why certain things are/aren't true. This doesn't apply so much for "yes/no" solvers, like SAT/SMT/resolution/etc. but is often the case for "interactive" systems like Coq/Agda.