> Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. It's quite difficult to look at systems like Dafny or {J,C}BMC, in particular, and say

> Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. It's quite difficult to look at systems like Dafny or {J,C}BMC, in particular, and say "they can only show a _specification_ is sound, but not the _implementation_.", since those systems are definitely saying something about the implementation. Regarding "soundness", I think you're confused about terminology. I have no idea what it would mean for a spec to be bug-free; that seems equivalent to saying that a program is bug-free. Specs can have bugs for the same reason that implementations can have bugs. Anyways, "sound" has a well-understood meaning that is quite different from the one you're imposing. Soundness is a property of the entire system, not of individual formulas (specifications). A formal system/tool is sound if the system only admits proofs of a formula F whenever F is valid in the semantics. > But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question. You're missing the point, which are the ellipses. OP's question is "are formal methods worth it for me?" The appropriate answer has NOTHING to do with the type of code that OP is writing or their application domain. AWS components are not safety-critical in the sense of aircraft or automotive software, and they run on commodity hardware. Ditto for financial systems. But formal methods are applied successfully in both contexts. Again, I've used hand-rolled formal methods for Django apps as part of our deploy process and it's definitely saved us headaches. The implementation effort took very little time. A weekend and then a bit of ad hoc follow-up work. The rise of amazing parsers, really good implementation languages for this sort of code (scala, F#, ocaml), and fantastic SMT solvers (particularly string constraint solving) means that what used to require a "huge investment" can now be done in a weekend hackathon. Hardware is also making formal methods a cheaper prospect. Lately I've been playing with a small cluster of 64 core processors during off-hours and the amount of brute force search you can do in a weekend is pretty incredible. Formal Methods are often cheap and easy to implement, but they do have a high up-front human capital cost/learning curve. You need to know how to coalesce a class of bugs into a mathematical description. And then how to check that mathematical description against code by hacking together parsers, AST rewrites, and SMT solvers. The idea that this takes months or years of even weeks of time is pretty dated. A learned hand can get a lot done in a weekend.