Why Formal Methods Remain Unused Despite Their Potential
Why Don't People Use Formal Methods?
I explore the historical and practical barriers preventing the widespread adoption of formal methods in software development. While often dismissed as too expensive or unnecessary for non-critical systems, the real challenges lie in defining precise specifications and the steep learning curve required to translate human concepts into mathematical proofs. I argue that despite these hurdles, formal verification offers unique value in preventing crashes and security flaws that traditional testing often misses.
People assume that formal methods are widely used in high-assurance software and unnecessary for everything else; this, if anything, is too optimistic, as most people in high-assurance software don't actually use formal methods.
- malisper
I recently came across a use case where formal methods were incredibly helpful. I've been rewriting Postgres in Rust and am currently focusing on correctness. The biggest challenge is that there's so much surface area to cover. Postgres has over 3000 user-facing functions, ranging from regular expression matching to JSON iteration to computing the gamma function. About half of these functions are simple pure functions.
Of the 3000 functions, I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior for over 1000 of them. In the process, I found 4 different Postgres bugs. All of them would not be triggered under ordinary usage, but one, if triggered, would corrupt your database.
I think why formal methods works well for this is I'm testing a large number of small to medium self-contained pieces of code. For each of them the specification is simple: does postgres_fn(args) == pgrust_fn(args). I've been using Kani[0] which works across both Rust and C code so the proofs are based off the actual code and not a translation of the code to another language.
If you want to check out what all the verification look like, you can see them here[1]
- teiferer
To me, "this returns sorted lists" illustrates the crux.
You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is what a formal specification is) that needs to be checked against what we actually want. And that "code" needs .. a test? Hard thinking? A formal verification itself?
Don't believe me that this is hard? Back to "this returns sorted lists". The promise of formal verification is that whatever implementation I throw at the verifier, as long as it passes the check, I'm happy (assuming that I can also encode things like running time and resource use). Now imagine a program that always returns the empty list. It satisfies "this returns sorted lists" trivially but is not at all what we want. The formal spec has a bug. Such issues can be subtle in larger projects and no amount of model checking or SMT solvers can guard you against a bug in that "code".
Don't get me wrong, it can be incredibly useful. But it's not the silver bullet that some proponents make it out to be. It's another tool next to testing, not instead of it. (The whole "testing can only prove the existence of bugs, not their absence, that's why we should use formal verification instead" is just misguided at bes […]
- ndriscoll
We do. It's called a type checker. Every "formally verified" system is going to be partially verified. e.g. you might prove your sort procedure sorts, but did you prove its complexity? Under a cost model for integer compares or a cost model for page fetches? Or both? Multi-layer cache page fetch costs? How well you verify just depends on how well you decide to model the problem. Different type checkers have different modeling features.
This is a more useful perspective; it's not "we do/don't use formal methods," but instead "how can I more precisely model my domain?" Helpfully, if you model your domain well, code tends to be obvious/write itself.
- SCdF
In most industries that need software made for them it's hard enough to get people to care about spending enough time on informal methods let alone formal ones. I simply don't think most of the industry has had the breathing room and respect for engineering for this pattern to develop.
- scrubs
A little self promotion: for a way to see how to use TLA as a formal method see:
https://news.ycombinator.com/item?id=48287718
I give a comprehensive introduction to formal methods without assuming background with a constant emphasis on examples, and using the tool.
- asxndu
I think it's the culture is software engineering.
In a food delivery app/social network it seems like a waste of time to use formal methods.
When designing software for aircraft, pacemakers, fintechs, cryptography and DeFi protocols there is a bit of value for formal methods.
The problem is that often, people with the food app/social network culture are hired to build DeFi protocols.
Which explains why so much money is being stolen form DeFi protocols of late.
So why people don't use formal methods.
- 95% of the time, the stakes are low
- 5% of the time, the engineers don't understand the value of formal methods.
Leslie Lamport once joked that if software developers were architects, they would first build a skyscraper and then later draw the blueprint.
- s_dev
https://blog.janestreet.com/formal-methods-at-jane-street-in...
I thought this article from Jane Street makes a nice complimentary pairing.
- tombert
I've been a big nerd for formal methods for quite awhile, and have been broadly unsuccessful in getting employers onboard.
I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason whenever I have tried proposing TLA+ in the past, people will nod along and wait for me to stop talking. I've had several managers say "they'll look into it", which was such an obvious lie that I don't know why they even bothered.
I've "snuck in" TLA+ usage a few times. I gave up on getting anyone else to use TLA+, but as I've gotten more senior-level, I have been given a fair bit more leeway on how I approach projects and as such I have been able to budget myself a day or two to model some of the less-obvious bits of concurrency.
All that said, I have had some luck with designing stuff with TLA+, then feeding the spec into Claude and getting that to implement the actual executable code. Maybe I'll be able to convince an employer that's a good use of time now.