Strongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done.
Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).
Lean has dependant types. Wouldn't something like Haskell or Idris, that are trying to be general purpose dependantly typed languages--wouldn't they be a better start than versus?
Versus appears to just be a formal verification tool. Perhaps I misunderstand?
You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used the most (long ago), and the tooling was interactive in a helpful way I've never experienced with other languages.
You don't want a separate language used to verify a base language, because then everyone ends up having to know two languages. Looking at the history of computing though, I wouldn't be surprised if this happens.
The actual programming language and the verification language can be the same language though, if we want.
in case anyone's interested i have a vibe coded fork of verus that replaces the verus-the-language side of verus with plain old Lean 4. It's still two languages, but now at least the second language is as mainstream as it gets in the field and has good automation. i haven't finished wiring up the Lean 4 infoview and vs code extensions and LLM skills into it yet, which makes it not as easy to write yet as lean 4 with the IDE bells and whistles.
I'm also playing around with using the lean's compile-to-C tooling to instead compile to rust instead and it's getting more of my focus than the lean-via-verus route right now.
if people are interested, ping me and i can put them up on gh.
As a meta-comment on the topic, something I have noticed is that there still exists confusion what it means to use theorem provers for projects -- the other day I read a tweet from Paradigm, a crypto-VC now seemingly AI-pilled. Some LP of theirs had made a Lean 4 formalization of the Ethereum's virtual machine. The tweet said this would have cost like $150k in API tokens ("would have", as in, I guess they get theirs for free), and took a week of inference time for an LLM to produce. I somehow got distracted to actually take a look at the code, which I found rather light on theorems. Nor did the project make use of Batteries or Mathlib which are arguably the one of the strongest motivation for me personally to use Lean4. That is, I generally rather rely on someone else getting the category theory and algebraic structures right, which then leaves me the proof obligation to show the correspondence with whatever toy I'm working on. Here I'm fine to use LLMs for proof search, very similar to how would I use a SMT solver. But what I have found is that the language models have to be really coerced into using these libraries, because otherwise the models much rather overfit and overclaim a solution with a 3 minute inference task rather than attempt to fulfill the proof obligations over 3 hours. And I feel nauseated when I need to convince the LLM (I use Claude) that filling the proof obligation is for "academic exercise" or because I'm coerced into doing so, because otherwise it will come up with reasons of its own why it does not want to do it. Now, this happens under the mental model in which I'm interested in finding equivalences with prior work. Many LLM generated Lean code reads more as if someone was interested whether X can be turned into a Lean 4 program, which is mostly yes, and that in general is a positive thing. But, if you are not interested in refinement types and theorems, why not just choose Haskell? The point is, I strongly sense that unless you have good questions to ask, then that's very evident in these languages. And, this is something the LLM won't help you -- if you don't impose a proof obligation for it, it certainly will not try to go the extra mile to conjure one for you.
I'm very bullish on proof automation as well. I'm currently researching AI for algorithm design and using automated theorem provers to get formal guarantees for generated algorithms.
To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback!
I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others.
This is really cool stuff, and I agree the future is likely to look more like this. I was surprised by the last two paragraphs ("Aside: verified assembly") -- my understanding was that this future is basically already here. I believe agl's colleagues at Google have already deployed some auto-mutated verified assembly versions of some crypto routines, based on the Fiat Crypto + CryptOpt work (https://arxiv.org/pdf/2211.10665), both involving Andres Erbsen who I think is currently at Google before starting a professorship soon. I dunno if this work would count as "cheap" (it looks like Fig. 10 unfolds over the course of a day) but spending a day auto-exploring many verified-correct machine code implementations of the same routine to find the fastest one (which you then ship forever) doesn't seem impractically expensive either.
Cool. Now we can write bugs in our theorem descriptions instead of source code.
Seriously, please review Curry Howard Isomorphism if you’re getting pulled down this rabbit hole.
Programs are proofs. Proofs are programs.
So if you can formally describe the correct output for every input, you can have an LLM loop automatically fill in the gaps of how to get there. Congrats, that sounds at least as hard as writing the correct program in most cases.
Don’t get me wrong, I do think there are useful tools combining formal methods and llms. Let’s just not get carried away.
> Congrats, that sounds at least as hard as writing the correct program in most cases.
That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use.
I can write a formal description of what it means to have property in a way that does have computational content that is equivalent to an algorithm[0], but often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted.
The magic is that you can write a spec that's clear, then have the LLM write the code and prove the spec, so you know that given the right inputs/state, it will return the right outputs/state. Then the gap is performance-like characteristics, which is a pretty great starting point and a lot easier to be just empirical about than correctness.
[0] in Lean you can also use classical logic or add your own axioms, where it's not even comutational.
> We now have LLMs which, combined with proof irrelevance, promise to be an extremely capable form of proof automation. With sufficient amounts of automation perhaps you don't need to worry about proof engineering nearly so much. You still need to avoid blowing up the type checker but, in my limited tests, LLMs can avoid that. Potentially, LLMs suddenly make dependent-type systems dramatically more practical.
When I've used interactive proof systems like Roq, I'd often kinda code myself into a hole by cutting along the wrong axes and not specifying my problem in a way that's easy to prove. After all, this is just like in math: you really want to cut at a problem the right way to get to the easy proof.
I think people are discounting how important that decision making is. It's not just about whether an LLM can churn through specific proof strategies on a problem, but also about how to pose the problem etc.
I'm not saying LLMs can't help, but I think it's less that "proof engineering is not needed" and more that "when these tools are used in the right way, proof engineering is easier". Because at the end of the day these tools work well when they have the right kind of foundations in the first place
> AWS made LNSym: a semantics and simulator for AArch64. That's cool. Perhaps we could use it to show equivalence between an optimised assembly implementation of some functions, and their Lean counterparts, and then use the assembly code at run-time? Then we could let LLMs rip at optimisation and they couldn't introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap?
Trying to one-shot compcert might be hard! Thinking about it and planning it out might make it easier though...
I agree with the core thesis that LLMs + theorem provers might make formal methods cheap enough to be practical in software development.
The biggest issue was always cost. But there's still an alignment problem. Without human supervision, things might drift away from the original specification and intent.
From my own experience, what works best is some kind of Hoare/separation logic (contracts), as these are quite easy to follow and decompose.
Even something as simple as a minimal Haskell subset, plus a bit of LiquidHaskell, can get you really far if you are pragmatic.
IMO the biggest issue was always not knowing what correct is in the first place. The vast majority of software we use, the stuff that's riddled with errors, has those errors largely because what it's supposed to do is vague and never, ever deals with edge cases. You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.
Perhaps that's the same thing as what you're saying, though: we don't specify these things in detail because it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.
This can work for core algorithms for sure, but wondering if this will work for production use cases, production apps come with a lot of edge cases - which are more often than not not logical as well to the point it becomes very hard to document them all in the first place.
The flip side is that we currently put programs into production without understanding how they will behave in those edge cases. If you're lucky, they crash and then restart cleanly. If you're unlucky, they silently corrupt data or violate mission-critical invariants.
Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).
Versus appears to just be a formal verification tool. Perhaps I misunderstand?
You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used the most (long ago), and the tooling was interactive in a helpful way I've never experienced with other languages.
You don't want a separate language used to verify a base language, because then everyone ends up having to know two languages. Looking at the history of computing though, I wouldn't be surprised if this happens.
The actual programming language and the verification language can be the same language though, if we want.
I'm also playing around with using the lean's compile-to-C tooling to instead compile to rust instead and it's getting more of my focus than the lean-via-verus route right now.
if people are interested, ping me and i can put them up on gh.
To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback!
I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others.
[1] https://github.com/henryrobbins/open-atp
[2] https://news.ycombinator.com/item?id=49010310
[3] https://news.ycombinator.com/item?id=48780801
Seriously, please review Curry Howard Isomorphism if you’re getting pulled down this rabbit hole.
Programs are proofs. Proofs are programs.
So if you can formally describe the correct output for every input, you can have an LLM loop automatically fill in the gaps of how to get there. Congrats, that sounds at least as hard as writing the correct program in most cases.
Don’t get me wrong, I do think there are useful tools combining formal methods and llms. Let’s just not get carried away.
That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use.
I can write a formal description of what it means to have property in a way that does have computational content that is equivalent to an algorithm[0], but often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted.
The magic is that you can write a spec that's clear, then have the LLM write the code and prove the spec, so you know that given the right inputs/state, it will return the right outputs/state. Then the gap is performance-like characteristics, which is a pretty great starting point and a lot easier to be just empirical about than correctness.
[0] in Lean you can also use classical logic or add your own axioms, where it's not even comutational.
When I've used interactive proof systems like Roq, I'd often kinda code myself into a hole by cutting along the wrong axes and not specifying my problem in a way that's easy to prove. After all, this is just like in math: you really want to cut at a problem the right way to get to the easy proof.
I think people are discounting how important that decision making is. It's not just about whether an LLM can churn through specific proof strategies on a problem, but also about how to pose the problem etc.
I'm not saying LLMs can't help, but I think it's less that "proof engineering is not needed" and more that "when these tools are used in the right way, proof engineering is easier". Because at the end of the day these tools work well when they have the right kind of foundations in the first place
> AWS made LNSym: a semantics and simulator for AArch64. That's cool. Perhaps we could use it to show equivalence between an optimised assembly implementation of some functions, and their Lean counterparts, and then use the assembly code at run-time? Then we could let LLMs rip at optimisation and they couldn't introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap?
Trying to one-shot compcert might be hard! Thinking about it and planning it out might make it easier though...
But every time I use Codex unless I specifically give it the abstractions it writes code that is way too specific.
The biggest issue was always cost. But there's still an alignment problem. Without human supervision, things might drift away from the original specification and intent.
From my own experience, what works best is some kind of Hoare/separation logic (contracts), as these are quite easy to follow and decompose.
Even something as simple as a minimal Haskell subset, plus a bit of LiquidHaskell, can get you really far if you are pragmatic.
Perhaps that's the same thing as what you're saying, though: we don't specify these things in detail because it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.
But still no P=NP.