Why don't people use formal methods? (2019)

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]

[0] https://github.com/model-checking/kani

[1] https://github.com/malisper/pgrust/tree/main/proofs

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 best and propaganda at worst.)

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.

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.

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.

https://blog.janestreet.com/formal-methods-at-jane-street-in...

I thought this article from Jane Street makes a nice complimentary pairing.

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.

This blog is actually very useful... There's also the flip side, possibly due to the expense (technically, intellectually, and emotionally), where "IT'S FORMALLY VERIFIED!!" has become some marketing code for "it's safe, secure, and PFAS free..." - just because something is formally verified, doesn't mean it's secure or fit for purpose. It usually just means it conforms to a given spec "and that's that..."

Pretty much every job I've had has involved integrating with highly imperfect, changeable, and inaccurately implemented (and barely documented) third party APIs. That's where most of the work went and I don't see formal methods improving the situation any time soon.

I was exposed to Z notation in the late 80's, and could not for the life of me see how to apply to my work as a junior programmer. But the distinction the OP makes between Design and Code Specification was lost on me then (and, I think, on the folks I knew who were looking at Z); and the OP indicates that Z is aimed at Design Specification. As a junior programmer, it's no wonder it was lost on me.

Speaking for myself (and I bought Hillel's recently published Logic for Programmers): It's not clear to me which formal method I should use. I'm certain the answer is "there's a different best one for each situation", but I don't want to know one for each problem I'll face. I'd rather have a definitive answer to what is the second best for all situations, similar to how we can answer "python" to that question when the question is about general programming

My 2c I don't understand any of the material I've read describing them. What I do understand makes them sound like it will be a load of work for questionable benefits. If I end up writing safety-critical code. (Aerospace firmware, big robots etc), I will get over this hump and learn them. If not, I am not yet compelled; rather intimidated.

Maybe this is like Quaternions, that are actually very easy and useful, but suffer from confusing descriptions. Or maybe more like Monads, which are actually very abstract, and may not be suitable unless your the sort who understands Mathematician style mathematics.

More to the point: I'm not even sure how I would get started and evaluate them tacitly.

Of particular confusion: Does formal verification lead to a strange-loop style or "It's verification all the way down" scenario, where you are shifting the correctness from the original code to the verification? Then must verify the verification ad-infinitum? (This is almost certainly wrong, but I don't grasp why)

The big question I ask: "Would I rather have a code base with formal verification, or one in which all the time and effort used by add that were spent using and testing the software in a practical way; or code reviewing it"

I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.

Because there is almost never a business need?

Most programs don't need to be rigorously perfect. If they did, LLMs wouldn't be as popular as they are right now.

If you're dealing with medical equipment or space flight, maybe there's a need. But usually the goal is to make errors _inexpensive_ to find and fix, not theoretically impossible.

Isn't the problem with formal methods that it isn't clear whether or not most of the useful code we use are actually formally verifiable?

The article mentions NP-complete, but is it actually a solvable problem in general?

> For extremely restricted cases, like propositional logic or HM type-checking, it’s “only” NP-complete.

Has anyone been experimenting with AI and formal methods - verification, proofs, or anything else? I've been thinking about this space quite a bit lately. For sufficiently interesting AI generated software, AI is also incapable of reviewing it - possibly for the same reason that humans are. AI ought to be able to adopt the formal methods humans have used to work around the inability to verify something just by looking at it hard. If the cost of adoption is what stopped us, thats no longer an issue.

When I interviewed at AWS, I asked this question directly to their formal methods expert. Her response was two-fold:

1. All our code changes too much, we wouldn't be able to formalize it before it needed to change.

2. We already did this where we could, you just don't see it.

I didn't get the job and remain very skeptical on both answers. I think they just didn't have enough power internally to change the move fast and break everything culture for the better.

"Much of this is a consequence of designs are not code. With most design languages, there is no automatic way to generate code"

Maybe now there is, but I don't know how good LLMs are at using these relatively obscure (at least to me) design languages.

Where formality, when right, still goes wrong:

0) premature but fitting;

1) settled but situationally mismatched;

2) same formal token, different external meaning.

I would say the tooling plays a part. Where are the go-to open source solution that a beginner can turn to without too much research?

I think everyone knows the answer already - it's too hard to be worth it for most problems. The article doesn't disagree with that and was a good read anyway. Don't skip it because you already know the answer.

IMO the reason is way more on the "it's too hard" side than "it isn't worth the effort". Formal verification is extremely common in the silicon hardware design world, despite its extreme cost (the tool licenses cost on the order of $100k per seat, as far as I can tell). And in this domain bugs are really expensive. But I think it would be used in spite of that simply because it is an order of magnitude easier than software formal verification.

I don't know if there is any solution to that. Software itself is an order of magnitude (or more) more complex than hardware... I think the author's suggestion of partial verification is the way to you. You're not going to formally verify your GUI but you could formally verify your LZ4 decoder. Maybe.

Interesting read, thank you. I share your goal, and I think with AI- coding proving code right has become more relevant than ever.

What prevents that we, just move the goal post? Moving the bug from code to spec? The spec must always be simpler and more easily to understand and debug than the code. But in praxis that means it can’t be fully specific in most of the use cases?

(Edit: replied to wrong comment)

For me, I wish the systems languages I am interested in could couple with legible verification systems, but alas, the world of formal methods seems disjoint. The only way to get a satisfactory development experience seems to be to learn Lean.