> I found 4 different Postgres bugs.

Bugs in the upstream Postgres C implementations? Did you report them or submit patches? I'm curious to see what you found!

> I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior

I thought you wanted to get rid of the bugs!

> I've been able to formally verify that the Rust behavior is identical to the Postgres C behavior for over 1000 of them.

Since both Rust and C have LLVM IR intermediates, you could use KLEE[0] for this.

[0] https://klee-se.org/

This guy is the real thing.

While there is certainly quite a bit of truth to what you say, I have a few counter arguments:

> same order of magnitude as the code implementing it

I believe mathematically formulating what an algorithm should do is very often orders of magnitue simpler than implementing it. As we know from the halting problem, it is easy to specify what the algorithm should do, but it is provably impossible to implement such an algorithm, so there the ratio of complexity is infinite ;)

Also, the huge advantage of a specification is that it is much more compositional than actual code. As the article states, one can just specify (and verify) that the code never crashes totally independent from what the code otherwise should be doing. So one can easily look at each part of the specification and understand why it is a desirable property piece by piece, in much larger isolation than the monolithic totality of the code.

Even more, with a formal specification one can (and probably should, when it gets too compilcated) verify by proof that the spec is internally consistent, i.e. that no part contradicts the requirements of another.

I think every formal methods phd student who's interested in adoption of their techniques/tools has a short bout of doubt/depression upon realizing just how large of a surface area for bugs lives in a sufficiently useful specification.

This is deeply related to the conceptual error a lot of executives are currently making around automation in/of their software engineering orgs.

It has always been true that learning some formal methods probably makes you a better programmer in certain ways, even if you never use them. I think it's increasingly also true that learning some formal methods probably makes you a better manager of people/processes that product software.

I was attending a conference back in, oh 2017 perhaps, where a few people from Microsoft were discussing their experience adopting TLA+ and somebody made the comment that they found that creating a spec was an exercise that could only meaningfully be done by the engineer (or perhaps team) writing the code. You wouldn’t, say, have an external TLA+ expert write the spec for you, but instead you would use the process of authoring the spec to ultimately learn more about your own design. And of course, perhaps avoid edge case bugs before they are written. Say what you want about Microsoft, but their observation does have a rather large sample size, and it sounded like formal methods was considered more impactful during software design rather than as software verification.

I have a deeper problem. When I'm calling sort() it is useful that it returns a sorted list. However my program rarely has sorted lists of any sort in any requirement. My requirements are around the features my users care about. Sure the list of employees that I need to display needs to be sorted (sometimes by hire date, sometimes by title, sometimes by name - and often combinations of the above), but there are a lot of things I'm doing with that list that are not sorting.

I mean, just for this particular example, you could certainly also add a check that the sorted list is the same length as the input list.

That said, your broader point is more or less correct. I think the advantage of something like TLA+ is that the specs can generally be more abstract and as such the checks can be more exhaustive than you would likely get with regular "code".

With concurrent code, in particular, it can be difficult to know if your algorithm is correct, especially without the confounding variables that you get with a "real" programming language. Is my program broken because of some memory allocation quirk? Is it broken because of some peculiarity with how pthreads are dispatched? Or is my design wrong? Being able to work at an abstract level at least can check the last part.

Of course, though, you are correct that formal methods aren't silver bullets.

I've been using TLA with claude code at work and it roughly takes twice as long, but it's already _fast_ to get claude to produce code and this prevents a lot of rework.

> The promise of formal verification

The promise of formal verification (and testing) is essentially the same promise as double-entry accounting. It assumes that if you do the same thing twice that it is unlikely you will screw it up in the exact same way twice. When there is disagreement it tells you that something went wrong, but you still need to look at both sides to determine which one is wrong. There is no such thing as a panacea, of course.

> It's another tool next to testing, not instead of it.

Theoretically it is instead of. They both are trying to solve the exact same problem. The real world with real constraints isn't so neat and tidy, so they don't end up perfectly overlapping.

One of my favorite quotes on this topic is:

"Type systems are just the parts of formal verification we've figured out how to make fast."

I think there's an element of this which really breaks down to the type system being the part of formal verification that we've figured out how to do during the course of implementation.

Software engineers (myself included, over the years) often argue their real value isn't just writing code, its figuring out the gaps in requirements and how to resolve them. Sometimes that engineering process gets turned back into a formal spec. But much more often, the implementation functionally becomes the spec and contains many details that were never present in the original statement of the requirements.

Formal verification techniques in general are a harder sell until we get the industry to a point where there's broader agreement that what we call "implementation" is often a blurry mix of spec development, prototyping, and actual implementation all happening at the same time.

I think programmers in general do not give much thought to the level of engineering required for a task.

Mostly, there's too little, but there are many cases when there's too much. I see people writing tons of tests for corporate software that will be used by a couple of people and will have to be updated regularly anyway.

Building a hut is not the same as building a skyscraper, but we don't really have guidelines for different software projects. No methodology I've ever seen distinguishes types of projects by complexity.

I think its also about tolerance for failure. For software that must not fail or where reliability commands a premium you would be wise to invest in formal methods. Core systems at aws for example. For throwaway CRUD code its just easier to try iterations on the problem and call it a day. Its not about respect just RoI.

Also you can write a perfect specification get into implementation and have to step back and redesign.

Software is fast to iterate and test that a lot assumptions can be proven by actually writing the code.

Software is closer to gardening or painting. We discover a lot through practice and writing code. Then we can often write more formal specifications.

But formal method is impractical for most software upfront, and instead is likely used for more serious runtime failures or cost of life.

That's just my two cents.

I enjoyed this quote from the article, which concisely summarizes the first part of the above comment:

> “website isn’t airplane!!!”

Software engineers are rarely engineers at all, and pretty much never know anything about computer science.

> 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

I think it's not only SWEs, but general persons that goe to college primarily to get a job, without having a natural curiosity for things.

That is always my problem too. I can see how to prove sort, if I was writing the standard library for my language I might do that (it is hard, but I hope whoever wrote my library did). However sort is already in my library. I'm writing code that does things much harder to write into a spec.

My guess is that the formal spec for a basic TODO list app is the same size as the source code of the app itself.

> 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?

IANA formal methods guy, but my understanding is: yes, you're shifting the correctness burden from the code to the spec.

So why is that better? Because the spec is much shorter and more focused -- it strips out all of the implementation details.

It's bad to say "you have to trust this 100,000 line program." It's much better to say "you have to trust this 100 line spec, and the code that verifies it."

> similar to how we can answer "python" to that question when the question is about general programming

An ironic claim in the context of formal methods.

The ironic thing is that LLMs are what will make formal methods feasible.

First: LLMs find so many bugs and security holes in software right now. So you pretty much have to prove your stuff correct, if you don't want to get hacked into.

Second: LLMs make it much easier to apply formal methods. Just ask Claude to prove your stuff in Lean or whatever, no PhD required anymore.

I'm not sure how to think about what you mean by "almost never." If most commercial software is web frontend + monolithic app code + relational DB, then you may very well be right.

That doesn't quite match my professional experience, though - there are so many companies building databases, message queues, filesystems, and similar infrastructure. Sometimes they're internal projects, and sometimes they're commercial products. I've always felt that those systems would benefit from formal methods, since they're usually trying to provide strong guarantees to the application code on top.

No, lots of problems can be expressed in a way that can be verified. But complete verification of an existing implementation is essentially impossible.

That doesn't mean that formal techniques are not useful, far from it. For example, AWS uses a formally specified model to verify if an implementation is correct by looking at the telemetry. See e.g.

https://p-org.github.io/P/advanced/pobserve/pobserve/

This isn't something you could meaningfully do with standard testing techniques, and it very compositional, you can do it piece by piece.

I would say that most companies are just badly run, and blunder along stepping on mines periodically, making no effort to systematically manage risks. The uses for formal methods are often much bigger than verifying pure software components.

For example, the recent NTP outage at Telstra, a major telco, took their entire network offline, and major clients like railway systems were offline for days; the compensation will be massive. A fairly basic level of FMEA or robustness checking would have identified that (a) downsizing the people who maintained the NTP system expertise, (b) operating time as a SPOF, (c) running a telco as a retail chain, real estate investment portfolio, and marketing operation, with a subsidiary that does technology, results in fairly unbounded political and commercial liability.

Formal verification is also extremely common in the software design world, to be fair. Most programming languages in use have at least a primitive type system and even those that historically didn't are gaining them (e.g. Typescript, Python gradual typing, etc.)

The question is, as always, to what degree do the returns start to diminish. The Rust crowd laughs at Go's level of formal verification and says that their level of formal verification is the right level, but then the Lean crowd laughs at Rust's level of verification and says that their level of formal verification is the right level. The universe laughs at all of them. For crowds so concerned about mathematical proofs, it is funny that they end up right back at gut feeling.