I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT solver, the Oppen-Nelson simplifier. The harder stuff used the Boyer-Moore prover, which uses heuristics and previous lemmas to guide the theorem prover. The Boyer-Moore prover had to be helped along by suggesting lemmas, which it would try to prove and which would then be used for later proofs. That was the tough human job.
Later systems seemed to have less automation. What tended to go wrong with formal methods was that the people doing them were too into the formalism. I was working on this for a commercial project that wanted bug-free code, not as an academic. The academic projects tended to get too clever. They had the mathematician's bias of wanting a terse notation and not much case analysis. That's not a good solution. You want lots of automated grinding and don't want to need much insight. The clever people kept inventing new logics - modal logic, temporal logic, etc, - to avoid verbosity in paper and pencil proof work. That wasn't really all that helpful. The basic truth of this business is that most of the theorems are rather banal.
As the Jane Street people point out, there's a big advantage in having control of the language. You want the verification statements integrated into the programming language. In many systems, they're embedded in comments, in a different syntax than the programming language, or even in completely separate files. This adds unnecessary work. It's good to see them pushing this forward.
We were doing this too early, over 40 years ago. It took about 45 minutes of compute back then to build up number theory from a cold start with the Boyer-Moore prover. Now it takes less than a second.
[1] https://archive.org/details/manualzilla-id-5928072/page/n3/m...
I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs.
TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future.
[1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
[2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf
> Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way.
It sounds like what you think as positives are exactly the things parent comment thinks as negatives.
I used to work in this field myself long ago (academically and practically). The difficulty that OP didn't suggest much appreciation for is that the interesting spaces for automated verification -- especially of distributed systems, say -- require exploring the space of formalisms between the trivial proofs of propositional logic (SAT solvers) and the undecidable proofs of first or second-order logic (interactive theorem proving environments such as Isabelle and Lean). This is the incredibly large space occupied most importantly by the various modal logics, which allow for quantification over graph traversals. There are remarkably expressive logics where the decision problem remains tractable, such as the modal mu-calculus.
That is, precisely if one wants automated tools for verification the seemingly obtuse work on novel formal systems is necessary.
There's a big difference between wanting a succinct proof and wanting a succinct statement of the requirements. The easier it is to state the requirements, the more likely you have stated them correctly. Whereas succinct proof is not relevant for industrial purposes, as long as the proover has a small trusted kernel, it makes no difference to the reliability.
"Logic is to computer science and software engineering what calculus is to ... mechanical or civil engineering"
Things professionals rarely use in practice?
Thanks for the pointers to the papers.
One book which seems not that well known is Arindama Singh's Logics for Computer Science 2nd edition - https://www.phindia.com/Books/BookDetail/9789387472433/LOGIC...
For more details see author's webpage - https://home.iitm.ac.in/asingh/books.html
> TLA+, which has gained quite a lot of popularity
Why do you think that? Outside of just toy examples, and vague examples of "AWS uses that", I don't know of any actual code which has TLA. Most of the things you can do with TLA, you can do with informal math notation quite easily.
Do you have any real world long term usage examples?
We have a number of TLA+ models at Oxide. Here's one:
https://github.com/oxidecomputer/omicron/blob/8b0886dbd02229...
See for example https://www.mongodb.com/company/blog/engineering/conformance...
Human interpretebility and human construction is going to be really important for formal specifications.
My fear is that we will get inscrutable maths that will be guarded by tiny coteries of devoties. The different inscrutable notations will be mutually incompatible, understanding one will not really help with the others. Most people will simply write english statements that cannot be verified properly.
Worse even, people will get machines to formalise their statements, and will not understand the formalism or the proofs, but will take part in the theatre of verification and act shocked when everything explodes.
Have you looked at ADA Spark?
If you have does it match your intuition of how things should be done?
I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly.
So I would be interested in perspectives of people who have been down this route before.
I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If programmers are constantly translating between two notations, customer resistance will be high.
If you need to write functions as scaffolding for proofs, they should be written in the programming language. You might need some operators that aren't actually runnable, such as FORALL, but the syntax should be that of the programming language. If your specs look like
in a language with none of those operators, you're doing it wrong. That's the disease of falling in love with the formalism.The user should not have to tell the proof system things the compiler already knows. Whatever overloading and aliasing rules the language enforces should be known and handled in verification, too. We worked off the syntax tree produced by a compiler front end modified to handle the verification statements, not the raw source code. Ada Spark has different aliasing rules than Ada, for example.
One big problem is that object oriented programming came and went in popularity. You really want object invariants. You need some way to attach an invariant to a data structure. You also need a clear boundary where control enters and exits the objects. If the language doesn't have objects, you struggle with trying to express object type invariants in the proof language. You don't get the boundaries as part of the programming language.
A useful interface between the prover and the program is simply to use
in the middle of code to encapsulate complex proof goals. A should be provable from the preceding code using a SAT solver. B, when assumed true, should provide enough info for a SAT solver to proceed from that point. Now you need to prove by external means. That creates a well defined problem which can be given to something AI-like, backed by a proof checker, to chew on.Ada Spark has some features that violate these rules. Also, it's hard to find anything about Ada Spark newer than ten years old.
There's a fair amount of interest in verifying Rust. There's been some progress using Dafny. But "Dafny is not Rust. Using Dafny requires porting algorithms of interest from Rust to Dafny. This port can miss details and introduce errors." There's the impedance mismatch again. Verus looks more promising. It is more Rust-like in syntax, they get the SAT solver/AI prover distinction, and there's active development.
Thank you. That makes things clearer.
I especially appreciate the trick of asserting the intermediate truth to help the prover along.
As someone who writes software I very much agree that verification of asserts before run time (written in the language itself) is very approachable to a programmer.
In a similar vein I agree with the folks at Jane Street that aiming to rule out specific classes of bugs (as opposed to proving a program is entirely correct) is a very practical goal.
Have you looked at "Verified Design-By-Contract"? See the paper Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm by David Crocker here - https://www.eschertech.com/products/verified_dbc.php
David Crocker's Verification Blog - https://critical.eschertech.com/
Not who you asked but I took a quick look.
Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime.
At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use.
I think their approach will fail on modern encryption code because it takes too much control (loops) from the programmer.
Which paper did you read? The "Safe Object-Oriented ..." one that i pointed to or something else? Crocker's writings explain a lot more especially w.r.t. usage with C/C++.
See for example Can C++ be made as safe as SPARK? - https://www.eschertech.com/papers/index.php which identifies a subset and enhances it with annotations. This can be updated with his later article Contracts arrive in C++26! - https://critical.eschertech.com/2025/09/09/contracts-have-ar...
Also see articles under Proving C and C++ programs correct - https://www.eschertech.com/articles/index.php
Animats was bemoaning that OO has declined and that you needed object/DS invariants. I was pointing to the fact DbC has it all (people should always use the runtime checking approach) and with Verified-DbC you could do it statically too. Formal Methods can be done at various levels and a developer can choose and adopt what he feels comfortable with initially before graduating to fullblown heavyweight methodologies/tools. What is needed is developing Formal Method Thinking. See the paper On Formal Methods Thinking in Computer Science Education linked to here - https://news.ycombinator.com/item?id=46298961