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]
Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were:
0) When parsing a macaddr[0], Postgres uses sscanf with %x. %x can wraparound. This means SELECT '10000000aa:bb:cc:dd:ee:ff'::macaddr; will return aa:bb:cc:dd:ee:ff.
1) When parsing a tid[1], Postgres uses strtoul. The return value of strtoul is different across platform for the empty string. This means on some platforms Postgres SELECT '(,5)'::tid; will error and others will accept it.
2) Postgres missed an overflow check in it's cash type[2]. When running SELECT '-92233720368547758.08'::money / (-1)::int8; some platforms will error and other's will return the MIN value. Postgres does check for this for some of the other cash related functions, but it missed it for one of them.
3) When hashing the "char" type Postgres will cast a char to an integer[3]. On some platforms char is signed and on others it's unsigned. This means the hash of a char can be different depending on the platform. If you are using a hash index or hash partitioning on a char and move your DB from x86 to arm, the hashes will differ and your index/partitioned tables become corrupted. Note that this is special char type that you have to refer to by "char" that is separate from the typically used CHAR(n) type which is what you typically use, hence this would never come up under real usage.
The common pattern with all of these is they rely on C behavior that differs across platform (integer overflow, char signedness, strtoul). Rust is better about having more consistent behavior across platforms so these cases get flagged when the Rust code and the C code differ.
I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload. The docs tend to say "same hardware architecture". Though if they don't intend to support this case I think it's a shame if the pg_control checks allow the server to start after such a migration.
> I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload
I would be very surprised by that because that means replicating a database between the two platforms would lead to corruption.
btw, this bug breaks dump-and-reload too. If you use partitioning, each partition is dumped and restored individually. In this case though, you'll get an error when you try to restore the data because it's trying to put data in the wrong partition. That's better corruption, but still an issue.
Very cool project and good finds. What do you see as the end state for your project - do you think pg has a path to upstream, or would this be a fork?
Without knowing anything about the pg team, I would assume they would be hesitant to even consider an under the hood switch, just from a risk management perspective, regardless of test coverage and formal verification. But I could be wrong.
My goal is to build the best database possible. I'm trying to imagine what Postgres would be like if it were built today. I've been able to make a bunch of big architectural changes that the Postgres team has been talking about but hasn't yet made. For example, threads instead of processes and a vectorized executor.
I think everyone would agree the types of changes I'm making are good ones. The challenge Postgres faces is there's millions and millions of Postgres databases out there so they are focused on minimizing the risk of breaking any existing functionality over doing a big high risk rearchitecture.
I could see ideas from what I'm doing gradually making their way into Postgres, but I think the odds that pgrust (or any Rust code for that matter) gets merged into Postgres is close to zero.
these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+.
My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?
Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of
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.)
Actually, sorting a list is an example of something really easy to specify: for each pair of two elements, the one that comes first is less than or equal to the one that comes second.
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 think you probably got this, but spelling it out anyways for future readers.
The conceptual gap I'm referring to here has nothing to do with formal methods per se. It's just an analogous problem with the quanta of information required to state the spec vs the quanta of information required to state the implementation.
Namely: once your problem has enough of a certain type of essential complexity, there's not a huge delta between "a sufficiently specific description of the problem" and "the source code that solves the problem". The complexity of a sufficiently specific prompt approaches the complexity of the actual solution. At that point, the former does not have the purported benefit and the latter has a lot of huge benefits (determinism, modularity, etc).
When one is operating in that regime of problems, proposing that one can substantially automate the software engineering function has a real "I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question" feel to it.
One thing I should say though is that the spec has the luxury of being free of some constraints that the implementation has. For example, the functional spec of a sorting function could describe the shape of the required output without having to say how to arrive there. Or in more complicated cases it could afford an exponential simple algorithm to say that the actual implementation must be functionally equivalent. That may make it simpler because it's free of having to run in linear or whatever time complexity.
Yes, it's probably the most important trick in formal methods. Often surprisingly difficult to make it actually work, but when it does you can end up with a powerful tool.
In a past life I spent a lot of time on that sort of thing for control systems and RL. Spec says what not to do, reward says what to do, implementation can be arbitrarily complex wrt the spec.
There are many opportunities for an analogous move in LLM-assisted software engineering.
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.
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 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.
In which way is that a "deeper" problem? What you are doing with that data can also be expressed as a formal spec.
Sorting is just used as an example everywhere because everybody knows exactly what we are talking about without having to explain a lot, it has a somewhat easy solution space and everybody has implemented some form at some point, likely in school, for the same reasons . Of course real world software is more complex that that but that's not the point.
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 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
Thanks for this fantastic extension of my example, because that is still incomplete Input [2, 1, 3] and output [1, 1, 1]. Matches your revised spec, still wrong.
If multiple smart software engineers get this simple problem wrong, then how many corpses are burried in the average formal spec? Unless it has gone through rigorous review and testing. Which could have been done to the code to be verified, by the way.
You need that the output is a permutation of the input.
I agree with your larger point though.
Maybe as a last comment, few people actually write tricky concurrent stuff. Like lock-free data structures. There are niches where you gain a lot with a thorough formal spec and verification. But in many cases people should just use sth off the shelf that is already safe, or just use a big lock instead of trying to be smart.
> Thanks for this fantastic extension of my example, because that is still incomplete Input [2, 1, 3] and output [1, 1, 1]. Matches your revised spec, still wrong.
Yeah, I agree with the sibling comment somewhat that you'd probably want to make sure that all the elements are included as well. I do think you'd get much more exhaustive testing at the algorithm level than you'd get with "regular" code, even with unit tests. But sure, your broader point is right, passing the spec doesn't guarantee that everything is "right", and it can be misleading.
I feel like formal methods help when you're optimizing concurrent software more than anything. About a year ago I had a project that I wrote a naive version that was too slow because the initial version had a ton of lock contention. I wanted to rewrite it to use a less lock-heavy system but I wasn't 100% sure that my idea on how to speed it up would actually work. I ended up doing my design in PlusCal before I wrote the new version, and there were issues with my initial version (where in certain cases we could lose vital records), but fortunately I was able modify the design to fix it. I translated my design to Java and my new version was way faster.
I don't agree that a big lock is a good idea, but I do agree that people should, in general, use off the shelf things to handle this instead of trying to be cool. That said, occasionally I get into situations where those libraries aren't a good fit, or what they're doing is too slow.
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.
Been having LLMs make TLA+ models since the winter and it does work wonders for complex stuff, I guess for the same reason it works for humans: the process of building the model helps when designing the code even if the model is thrown away later (I keep mine though)
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.
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.
Thankfully this is no longer strictly true. So, I think the quote needs a slight adjustment, "Type systems and $THING are just ...", but $THING is not very well defined yet. Between "linters", and other relatively fast AST-based rule enforcers, some of which looking at higher order behavior, I think we now have an amalgamation of formally verified concepts that we can consider fast enough and sufficient exercised in practice that we are ever closer to widespread formally and dependably verified software.
Still, it's a long journey, and academic formal verification would always be, by design, a few steps ahead of what the industry can do efficiently in practice.
The field really needs more popularizers. I mean people or projects who can do "advertising" like, "if you add our linter to your CI/CD pipeline, you'll never have X class of bug ever again!"
given your experience on the topic, i'm curious: do you think that the reason we haven't figured out how to make other parts of formal verification fast is that, in general, programming languages expose each individual machine operation in the code, so the verification surface area is the combinatorial set over that? i've been working on a low level high opinion language, and its verifications are able to be checked in an extremely tight loop, largely because of the structure of the language itself.
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.
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 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 know few 100% unit test coverage, strictest typing to encode invariants fellas who's app is consistently broken and product makes less money than the bakery in my village.
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.
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.
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.
> designing stuff with TLA+, then feeding the spec into Claude
That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs.
Unless you feed the code back into something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?
I'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production.
I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors are different things, and of course this would be an issue even if it were humans writing the code.
If you use something like Isabelle then that has direct Scala and Haskell export. I like Isabelle but personally I find that for actual engineering problems it is often too cumbersome and TLA+ is much easier to get something done.
> would be an issue even if it were humans writing
I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion.
From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.
I've never used Lean, but as stated Isabelle has a code exporter as well; I was working with the Haskell exporter when I was doing grad school, and obviously Haskell is directly executable. It's a pretty neat thing, though it's still not perfect.
For example, a lot of mathematical types aren't actually directly translatable to programming languages. For some stuff, there is a "close enough" mapping to the type that works for most realistic cases, e.g. integers -> Int64. Other types become considerably more irritating; you might prove something with regards to all real numbers, but when exporting to a "real" programming language, there really isn't such thing as "real" numbers, since computers can really only do the rationals. You could export to float64, but then you're dealing with IEEE rounding, which may or may not be fine for what you're working on. You could use something like GMP (which is what I ended up doing when I had this issue) but of course you pay a performance penalty by doing that, and of course you're then trusting the correctness of GMP (though there is a verified subset, to be fair).
I feel like with TLA+, I am typically working on higher-level problems. Usually I'm modeling distributed systems, which sort of inherently requires an "opinion" for deployment.
How would I deploy this code? Erlang? Kubernetes? Docker Swarm?
How am I doing service discovery? DNS? YOLOing with raw IP addresses?
Suppose my model has a global function [1] that I'm writing to as a global shared store? Where does this live? Is this a local cache? Is this Redis? Memcached?
I could go on. The whole point of TLA+ is to write and test the algorithms, and very purposefully allows and encourages you to ignore details that aren't necessary to show correctness of your algorithm.
I'm not saying you couldn't do this, to be clear. You could absolutely create an exporter for TLA+, but my point is that it would require a good chunk of opinions and decisions to do it. You'd also need to ensure that the semantics of these things properly map to your model, else the exporter is only of debatable utility.
I think this is why there isn't really a serious exporter for TLA+. You just work at a different level with it, and I think there are just too many (kind of arbitrary) decisions that would have to be made in order to do anything useful.
[1] In TLA+, "function" basically means key-value map.
That's illuminating, thank you for a generous reply. The point about real numbers and their representation (or lack thereof) in programming languages is a great example of the gulf between mathematics and programming. I understand that for most languages, there can be no direct correspondence between a mathematical proof and the program that implements it.
In a recent discussion about the paper "How real are real numbers?" by G. J. Chaitin, someone mentioned that there seems to be a trend of a "computational" approach to mathematics on one hand, and from the other side, a "mathematization" of computer programming. With the rise of language models and their ability to generate correct programs, I imagine there is a pressing need to bridge the gulf between the two fields. Not only to verify the correctness of programs written in existing languages, but to design languages where that need for verification is taken into considertaion from the ground up, maybe close to Rust where the compiler refuses to compile a program that cannot be verified to be correct.
A common complaint about software engineering is that it is not "engineering" as a formal discipline; and about computer science that it is not a "science" (nor is it about computers, any more than astronomy is "telescope science" and biology is "microscope science" [^1]). It seems to me that a firmer grounding in mathematics, particularly in programming language design, would be helpful in improving the situation, so that software is actually "engineered" based on immutable truths and logic, and verified to be correct.
And how would the computational approach to mathematics influence it as a discipline.. Not sure but I imagine it may bring the field closer to a "science"?
Yeah, I've always been that "annoying math guy" for pretty much my entire career.
This has always irritated me, because I'm not entirely sure what engineers feel that they bring to the table over a high school kid who bought one of those "learn C++" books. I always thought the value-add was supposed to be a better understanding of the theory and computer science and internals of how computers work, but that was evidently wrong.
I've noticed that the "software engineers bragging about not knowing any math" trend appears to be dying, so that's cool, but now it has been replaced with the even more depressing "software engineers don't need to even need to know how to code anymore because you can just ask Claude Code to do it".
> 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.
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"
> 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."
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.
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.
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.
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.
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.
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.
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.
It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification".
So I don't think you can say it's common in the software world.
Specifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.
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?
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.
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
> 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!
Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were:
0) When parsing a macaddr[0], Postgres uses sscanf with %x. %x can wraparound. This means SELECT '10000000aa:bb:cc:dd:ee:ff'::macaddr; will return aa:bb:cc:dd:ee:ff.
1) When parsing a tid[1], Postgres uses strtoul. The return value of strtoul is different across platform for the empty string. This means on some platforms Postgres SELECT '(,5)'::tid; will error and others will accept it.
2) Postgres missed an overflow check in it's cash type[2]. When running SELECT '-92233720368547758.08'::money / (-1)::int8; some platforms will error and other's will return the MIN value. Postgres does check for this for some of the other cash related functions, but it missed it for one of them.
3) When hashing the "char" type Postgres will cast a char to an integer[3]. On some platforms char is signed and on others it's unsigned. This means the hash of a char can be different depending on the platform. If you are using a hash index or hash partitioning on a char and move your DB from x86 to arm, the hashes will differ and your index/partitioned tables become corrupted. Note that this is special char type that you have to refer to by "char" that is separate from the typically used CHAR(n) type which is what you typically use, hence this would never come up under real usage.
The common pattern with all of these is they rely on C behavior that differs across platform (integer overflow, char signedness, strtoul). Rust is better about having more consistent behavior across platforms so these cases get flagged when the Rust code and the C code differ.
[0] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[1] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[2] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
[3] https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload. The docs tend to say "same hardware architecture". Though if they don't intend to support this case I think it's a shame if the pg_control checks allow the server to start after such a migration.
> I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload
I would be very surprised by that because that means replicating a database between the two platforms would lead to corruption.
btw, this bug breaks dump-and-reload too. If you use partitioning, each partition is dumped and restored individually. In this case though, you'll get an error when you try to restore the data because it's trying to put data in the wrong partition. That's better corruption, but still an issue.
The physical replication docs say "the hardware architecture must be the same", though they don't define "architecture".
Very cool project and good finds. What do you see as the end state for your project - do you think pg has a path to upstream, or would this be a fork?
Without knowing anything about the pg team, I would assume they would be hesitant to even consider an under the hood switch, just from a risk management perspective, regardless of test coverage and formal verification. But I could be wrong.
Thank you for the kind words!
My goal is to build the best database possible. I'm trying to imagine what Postgres would be like if it were built today. I've been able to make a bunch of big architectural changes that the Postgres team has been talking about but hasn't yet made. For example, threads instead of processes and a vectorized executor.
I think everyone would agree the types of changes I'm making are good ones. The challenge Postgres faces is there's millions and millions of Postgres databases out there so they are focused on minimizing the risk of breaking any existing functionality over doing a big high risk rearchitecture.
I could see ideas from what I'm doing gradually making their way into Postgres, but I think the odds that pgrust (or any Rust code for that matter) gets merged into Postgres is close to zero.
For other interested spectators, I found this post by the author to be a good example of architectural changes in pgrust (along with motivations): https://malisper.me/the-four-horsemen-behind-thousands-of-po...
these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+.
My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?
Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of
[0] https://github.com/model-checking/kani
[1] https://model-checking.github.io/cbmc-training/cbmc/overview...
> 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.
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.)
Actually, sorting a list is an example of something really easy to specify: for each pair of two elements, the one that comes first is less than or equal to the one that comes second.
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.
Execs will often hand-wave away complexity as being irrelevant detail. And sometimes it is - especially if an urgent directional decision is needed.
The key skill - which is rare - is knowing exactly how much analysis to do.
Formal methods are appealing because they suggest that full analysis is possible. But formally proved programs can still have bugs!
I think you probably got this, but spelling it out anyways for future readers.
The conceptual gap I'm referring to here has nothing to do with formal methods per se. It's just an analogous problem with the quanta of information required to state the spec vs the quanta of information required to state the implementation.
Namely: once your problem has enough of a certain type of essential complexity, there's not a huge delta between "a sufficiently specific description of the problem" and "the source code that solves the problem". The complexity of a sufficiently specific prompt approaches the complexity of the actual solution. At that point, the former does not have the purported benefit and the latter has a lot of huge benefits (determinism, modularity, etc).
When one is operating in that regime of problems, proposing that one can substantially automate the software engineering function has a real "I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question" feel to it.
Well put, thank you.
One thing I should say though is that the spec has the luxury of being free of some constraints that the implementation has. For example, the functional spec of a sorting function could describe the shape of the required output without having to say how to arrive there. Or in more complicated cases it could afford an exponential simple algorithm to say that the actual implementation must be functionally equivalent. That may make it simpler because it's free of having to run in linear or whatever time complexity.
Yes, it's probably the most important trick in formal methods. Often surprisingly difficult to make it actually work, but when it does you can end up with a powerful tool.
In a past life I spent a lot of time on that sort of thing for control systems and RL. Spec says what not to do, reward says what to do, implementation can be arbitrarily complex wrt the spec.
There are many opportunities for an analogous move in LLM-assisted software engineering.
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.
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 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.
In which way is that a "deeper" problem? What you are doing with that data can also be expressed as a formal spec.
Sorting is just used as an example everywhere because everybody knows exactly what we are talking about without having to explain a lot, it has a somewhat easy solution space and everybody has implemented some form at some point, likely in school, for the same reasons . Of course real world software is more complex that that but that's not the point.
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 think you'd want to specify that every element in the original list is present in the sorted list (and in the same number, in case of ties).
And of course, that raises the issue of what do you want to do about ties....
> 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
Thanks for this fantastic extension of my example, because that is still incomplete Input [2, 1, 3] and output [1, 1, 1]. Matches your revised spec, still wrong.
If multiple smart software engineers get this simple problem wrong, then how many corpses are burried in the average formal spec? Unless it has gone through rigorous review and testing. Which could have been done to the code to be verified, by the way.
You need that the output is a permutation of the input.
I agree with your larger point though.
Maybe as a last comment, few people actually write tricky concurrent stuff. Like lock-free data structures. There are niches where you gain a lot with a thorough formal spec and verification. But in many cases people should just use sth off the shelf that is already safe, or just use a big lock instead of trying to be smart.
> Thanks for this fantastic extension of my example, because that is still incomplete Input [2, 1, 3] and output [1, 1, 1]. Matches your revised spec, still wrong.
Yeah, I agree with the sibling comment somewhat that you'd probably want to make sure that all the elements are included as well. I do think you'd get much more exhaustive testing at the algorithm level than you'd get with "regular" code, even with unit tests. But sure, your broader point is right, passing the spec doesn't guarantee that everything is "right", and it can be misleading.
I feel like formal methods help when you're optimizing concurrent software more than anything. About a year ago I had a project that I wrote a naive version that was too slow because the initial version had a ton of lock contention. I wanted to rewrite it to use a less lock-heavy system but I wasn't 100% sure that my idea on how to speed it up would actually work. I ended up doing my design in PlusCal before I wrote the new version, and there were issues with my initial version (where in certain cases we could lose vital records), but fortunately I was able modify the design to fix it. I translated my design to Java and my new version was way faster.
I don't agree that a big lock is a good idea, but I do agree that people should, in general, use off the shelf things to handle this instead of trying to be cool. That said, occasionally I get into situations where those libraries aren't a good fit, or what they're doing is too slow.
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.
Been having LLMs make TLA+ models since the winter and it does work wonders for complex stuff, I guess for the same reason it works for humans: the process of building the model helps when designing the code even if the model is thrown away later (I keep mine though)
> 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.
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.
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."
Thankfully this is no longer strictly true. So, I think the quote needs a slight adjustment, "Type systems and $THING are just ...", but $THING is not very well defined yet. Between "linters", and other relatively fast AST-based rule enforcers, some of which looking at higher order behavior, I think we now have an amalgamation of formally verified concepts that we can consider fast enough and sufficient exercised in practice that we are ever closer to widespread formally and dependably verified software.
Still, it's a long journey, and academic formal verification would always be, by design, a few steps ahead of what the industry can do efficiently in practice.
The field really needs more popularizers. I mean people or projects who can do "advertising" like, "if you add our linter to your CI/CD pipeline, you'll never have X class of bug ever again!"
given your experience on the topic, i'm curious: do you think that the reason we haven't figured out how to make other parts of formal verification fast is that, in general, programming languages expose each individual machine operation in the code, so the verification surface area is the combinatorial set over that? i've been working on a low level high opinion language, and its verifications are able to be checked in an extremely tight loop, largely because of the structure of the language itself.
Or, at least how to make easy to create. (What is related to fast in complex ways.)
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.
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 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 know few 100% unit test coverage, strictest typing to encode invariants fellas who's app is consistently broken and product makes less money than the bakery in my village.
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.
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.
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!!!”
https://blog.janestreet.com/formal-methods-at-jane-street-in...
I thought this article from Jane Street makes a nice complimentary pairing.
And it’s not just blogs. They’ve got an open job posting [0] for a ‘Formal Methods Engineer’.
[0] - https://www.janestreet.com/join-jane-street/position/8585303...
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.
> designing stuff with TLA+, then feeding the spec into Claude
That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs.
Unless you feed the code back into something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?
I'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production.
I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors are different things, and of course this would be an issue even if it were humans writing the code.
If you use something like Isabelle then that has direct Scala and Haskell export. I like Isabelle but personally I find that for actual engineering problems it is often too cumbersome and TLA+ is much easier to get something done.
> would be an issue even if it were humans writing
I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion.
From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.
I've never used Lean, but as stated Isabelle has a code exporter as well; I was working with the Haskell exporter when I was doing grad school, and obviously Haskell is directly executable. It's a pretty neat thing, though it's still not perfect.
For example, a lot of mathematical types aren't actually directly translatable to programming languages. For some stuff, there is a "close enough" mapping to the type that works for most realistic cases, e.g. integers -> Int64. Other types become considerably more irritating; you might prove something with regards to all real numbers, but when exporting to a "real" programming language, there really isn't such thing as "real" numbers, since computers can really only do the rationals. You could export to float64, but then you're dealing with IEEE rounding, which may or may not be fine for what you're working on. You could use something like GMP (which is what I ended up doing when I had this issue) but of course you pay a performance penalty by doing that, and of course you're then trusting the correctness of GMP (though there is a verified subset, to be fair).
I feel like with TLA+, I am typically working on higher-level problems. Usually I'm modeling distributed systems, which sort of inherently requires an "opinion" for deployment.
How would I deploy this code? Erlang? Kubernetes? Docker Swarm?
How am I doing service discovery? DNS? YOLOing with raw IP addresses?
Suppose my model has a global function [1] that I'm writing to as a global shared store? Where does this live? Is this a local cache? Is this Redis? Memcached?
I could go on. The whole point of TLA+ is to write and test the algorithms, and very purposefully allows and encourages you to ignore details that aren't necessary to show correctness of your algorithm.
I'm not saying you couldn't do this, to be clear. You could absolutely create an exporter for TLA+, but my point is that it would require a good chunk of opinions and decisions to do it. You'd also need to ensure that the semantics of these things properly map to your model, else the exporter is only of debatable utility.
I think this is why there isn't really a serious exporter for TLA+. You just work at a different level with it, and I think there are just too many (kind of arbitrary) decisions that would have to be made in order to do anything useful.
[1] In TLA+, "function" basically means key-value map.
That's illuminating, thank you for a generous reply. The point about real numbers and their representation (or lack thereof) in programming languages is a great example of the gulf between mathematics and programming. I understand that for most languages, there can be no direct correspondence between a mathematical proof and the program that implements it.
In a recent discussion about the paper "How real are real numbers?" by G. J. Chaitin, someone mentioned that there seems to be a trend of a "computational" approach to mathematics on one hand, and from the other side, a "mathematization" of computer programming. With the rise of language models and their ability to generate correct programs, I imagine there is a pressing need to bridge the gulf between the two fields. Not only to verify the correctness of programs written in existing languages, but to design languages where that need for verification is taken into considertaion from the ground up, maybe close to Rust where the compiler refuses to compile a program that cannot be verified to be correct.
A common complaint about software engineering is that it is not "engineering" as a formal discipline; and about computer science that it is not a "science" (nor is it about computers, any more than astronomy is "telescope science" and biology is "microscope science" [^1]). It seems to me that a firmer grounding in mathematics, particularly in programming language design, would be helpful in improving the situation, so that software is actually "engineered" based on immutable truths and logic, and verified to be correct.
And how would the computational approach to mathematics influence it as a discipline.. Not sure but I imagine it may bring the field closer to a "science"?
[^1]: I think attributed to Vinton Cerf in _Where Is the Science in Computer Science?_. https://cacm.acm.org/opinion/where-is-the-science-in-compute...
Software engineers are rarely engineers at all, and pretty much never know anything about computer science.
Yeah, I've always been that "annoying math guy" for pretty much my entire career.
This has always irritated me, because I'm not entirely sure what engineers feel that they bring to the table over a high school kid who bought one of those "learn C++" books. I always thought the value-add was supposed to be a better understanding of the theory and computer science and internals of how computers work, but that was evidently wrong.
I've noticed that the "software engineers bragging about not knowing any math" trend appears to be dying, so that's cool, but now it has been replaced with the even more depressing "software engineers don't need to even need to know how to code anymore because you can just ask Claude Code to do it".
> 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.
Probably true, I've just only ever worked in the software engineering world so I cannot speak about anything else.
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
> 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.
Out of curiosity, why’s that? I don’t know formal methods nor the relationship to python.
The most widely available, useful, and best-bang-for-buck formal method is using a good type system.
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"
> 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."
That is a great explanation!
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.
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.
> A proof of a basic todo list or something like that.
Just using a verb here would be a first step toward rigorous thinking. A proof that a todo list does what?
To-does. Just like how a butler buttles.
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.
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.
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.
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.
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.
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.
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.
It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification".
So I don't think you can say it's common in the software world.
Specifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.
As I said, it's a continuum. I'm drawing the line somewhere further along it than Rust's type system.
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.
> The only way to get a satisfactory development experience seems to be to learn Lean.
Or SPARK, if you want to stick to systems languages.