Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- > 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...
by rtpg - 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.
[1] https://github.com/henryrobbins/open-atp
- I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details.
Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was pointless and completely defeated the purpose.
(An LLM also pointed that out, so I guess it must have been a different one which implemented it? I'm trying to get them to sign their names in the commits...)
These new models are very thorough and responsible however, so of course it had written a copious number of tests, and of course all the tests passed! I found this very amusing. It had diligently proven the correctness of the incorrect functionality!*
I've been thinking about how cool it is the AI can assist with writing proofs now, and how we can use this new ability to boost the correctness of our code. It later occurred to me, however, that formal verification would not have helped in this case. It would have just formally verified that the wrong thing was correct!
--
*Yeah I know tests prove the presence of bugs but not their absence. Couldn't think of a better way to phrase that though.
by andai - 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.
- I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible.
Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, with more elaborate properties and longer proofs.
Suddenly, you realize that you need to prove a new property of your program. Can you keep your existing work and build on top of it? In general, no, you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.
That is because dependent types (and other staples of naive approaches to proving program properties, like a unique invariant per loop) structure the program along the wrong dimension: they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it") or a program point ("write the precondition for this function as a big conjunction mixing all the concerns"), where it works much better, for long-term maintenance, to structure the development along concerns: computational parts of the program, basic functional properties and absence of UB, termination, other functional properties, security, etc., where each layer builds on top of the previous ones without requiring them to change.
That is not to say that dependent types do not have their use. Where they shine is at module boundaries. Consider a library that exposes an opaque type and operations on it. Users of the library can only build and modify values of that type through the library's API. This type should be a dependent type. If it needs to be refined at any point to encode a new invariant, this will have no impact on the library's users, since all they do is pass around values without interpreting them. However, inside the library, I would recommend unpacking/repacking the dependent type at the library's entry points and handling the concerns separately.
- 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).
by gz09 - 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.by Jhsto
- Self-insert time.
I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost.
We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) So the cost of finding and developing exploits has dropped dramatically.
On the other hand, formal verification is now much easier, since LLMs can automate the proof. You don't even need to worry about hallucinations, you merely need to trust Lean core. If the LLM is wrong, the proof will get rejected!
The problem of exploits gets bigger, and the solution of formal verification gets cheaper. As a result, the needle is now moving in the direction of "more formal verification".
I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time.
My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly. I have not achieved that goal yet.
What I have so far:
- one (non-optimized) compiler step which is formally verified
- three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR
https://github.com/m1el/riscv-fv-bootstrap
The project is in quite a bad shape, and I am trying to improve my skills in that direction.
by m1el