Formal proofs of code are almost beyond the capabilities of the best human programmers (3.7 lines per day!), but LLMs can bash out code at an amazing pace. It's often crap, sadly, but the proof they are bashing out is the hard bit. If possible at all, the task is EXPTIME. Verifying the proof is only P, so when it's wrong you tell the LLM to do it again. A stable agentic loop is what makes it possible. The results in the article I linked to speak for themselves.
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.
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..."
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.
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
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.
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 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.
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.
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.
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]
I have also found that equivalent rewrites are one of the best applications for formal. Other examples can be things like vectorizing code while proving the vectorized version is formally identical, refactoring types or objects, or select classes of performance optimization that are not expected to change the output.
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.
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."
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.
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.
Almost all software is internal "make the business run" software that we never see, or web pages. Very very few engineers would even consider making a new message queue. The crowd here is different than most :)
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.)
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'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.
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.
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.
It's a complementary tool that replaces certain difficult types of testing. Viewed this way, you can focus writing formal specification for things which are easy & clear to formally specify. "this returns sorted lists" is, for example, a simple property. Other examples might be the O(n) performance of your algorithm. Meanwhile, "every input can be found in the output" might feel too painful to write, so you might compromise on "the output has the same number of elements as the input". This leaves plenty of space for classical testing, while unburdening classical testing from worrying about select classes of bugs.
One other valuable part of formal methods is forcing the author to make claims about their program, and then poking holes in those claims. This process helps the author understand their own code better, and after a process of iteration developing the formal properties that are actually true, you now have a strictly-true external interface specification for the program. This is obviously most-valuable for only certain classes of code, such as libraries or services.
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?
Because you can use it to find temporal errors in your software. People in fact do. So, that proves it's worth even if one can't be sure of perfect conformance to the spec.
Far as connecting specs to code, these papers did try to combine Event-B with SPARK Ada:
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.
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 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.
I believe I proposed that somewhere because it was a small, useful app which often opened malicious payloads. People may or may not fully prove it.
What I thought would be useful is, like Ironsides DNS, a SPARK Ada or other implementation that shows no code injections could ever happen from loading, modifying, or rendering text. That's a useful subset of full verification.
If not that verified, writing things in a memory-safe, concurrecy-safe language covers lots of ground. Rust and Pony put good effort in those areas. In Rust, I think you still had to manually turn on checks for some overflows which hurt performance a lot. So, static analyzers or automated provers for range properties have a performance benefit.
Muen is the largest, production project I know in such a language:
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.
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?
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.
53 comments
[ 0.22 ms ] story [ 17.2 ms ] threadI thought this article from Jane Street makes a nice complimentary pairing.
[0] - https://www.janestreet.com/join-jane-street/position/8585303...
Formal proofs of code are almost beyond the capabilities of the best human programmers (3.7 lines per day!), but LLMs can bash out code at an amazing pace. It's often crap, sadly, but the proof they are bashing out is the hard bit. If possible at all, the task is EXPTIME. Verifying the proof is only P, so when it's wrong you tell the LLM to do it again. A stable agentic loop is what makes it possible. The results in the article I linked to speak for themselves.
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.
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.
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.
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.
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.
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.
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 thought you wanted to get rid of the bugs!
Since both Rust and C have LLVM IR intermediates, you could use KLEE[0] for this.
[0] https://klee-se.org/
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.
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.
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"
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."
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.
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.
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.)
> 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.
One other valuable part of formal methods is forcing the author to make claims about their program, and then poking holes in those claims. This process helps the author understand their own code better, and after a process of iteration developing the formal properties that are actually true, you now have a strictly-true external interface specification for the program. This is obviously most-valuable for only certain classes of code, such as libraries or services.
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.
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?
Far as connecting specs to code, these papers did try to combine Event-B with SPARK Ada:
https://scispace.com/pdf/towards-generating-spark-from-event...
https://rd.springer.com/chapter/10.1007/978-3-031-23119-3_13
Or SPARK, if you want to stick to systems languages.
What I thought would be useful is, like Ironsides DNS, a SPARK Ada or other implementation that shows no code injections could ever happen from loading, modifying, or rendering text. That's a useful subset of full verification.
If not that verified, writing things in a memory-safe, concurrecy-safe language covers lots of ground. Rust and Pony put good effort in those areas. In Rust, I think you still had to manually turn on checks for some overflows which hurt performance a lot. So, static analyzers or automated provers for range properties have a performance benefit.
Muen is the largest, production project I know in such a language:
https://muen.sk/
Ironsides was an earlier project:
https://ironsides.martincarlisle.com/
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.
Maybe now there is, but I don't know how good LLMs are at using these relatively obscure (at least to me) design languages.
0) premature but fitting;
1) settled but situationally mismatched;
2) same formal token, different external meaning.
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?