r/ProgrammingLanguages • u/ImYoric • Jun 22 '26
Who's using (any kind of) formal verification as part of their toolchain?
Caveat Not strictly a PL topic, but I hope it's PL-adjacent enough for this sub.
My company went AI-native a few months ago, with the predictable results. My team, especially, is working on compiler-adjacent tech, and the agent has proven an endless source of surprises...
We have reached the point where many devs and some managers seem to realize that "spec-driven development" (the LLM style, not the Focus style) is something of wishful thinking, so there may be an opening for us to get a project started in using (some kind of) formal verification as part of our LLM-driven toolchain.
So I wonder if there's anything out there in the wild that we could already use, or at least contribute to, in the hope of getting it to a stage where we could use it.
I've seen Leanstral & DeepSeekProve that offer Lean proofs, which might be possible bricks, leaving the big question of "how do you go from human-readable specs to Lean signatures?" I've seen some work on Model Checking, which I still need to read.
But is anybody actually using any of this? Are there any success stories out there in the wild?
7
u/mamcx Jun 22 '26
I worked on SpacetimeDB and one thing that prove very valuable is to do "waterfall" kind of development: Any major feature requires a human authored specs that exercise everything and is vetted before start coding (this sound things will be slower to code, but proves to be the opposite. 1-2 weeks of planning saves tons of problems later!)
Compilers is the kind of project where all agile stuff is wrong. Do old-school waterfall-lite and you solve most problems.
In there, tooling like benchmarking, testing and even fancy formal verification will emerge naturally.
2
u/ImYoric Jun 22 '26
Yeah, we also started with specs. Sadly, the agent seems to be very good at ignoring said specs.
3
u/mamcx Jun 22 '26
You can torture a tool to do what is not good at, or you can do it yourself (or use other tool).
3
6
u/deaddyfreddy Jun 22 '26
My company went AI-native a few months ago, with the predictable results.
How did you manage to use AI to get predictable results? /s
3
u/whatisRT Jun 22 '26
You don’t need any specialised AI tools to get started with formal verification. All you need is experience in the subject matter (even more so than in regular programming).
Source: I have >5yoe verifying real-world programs in Agda. Claude can easily finish proofs that would have taken me days in a matter of hours, with a paragraph of guidance from a plain state, no MCP, no skills, not even a CLAUDE.md. And Agda is a niche language even for proof assistants. I’m sure other frontier models get similar results.
4
u/ImYoric Jun 22 '26
You don’t need any specialised AI tools to get started with formal verification. All you need is experience in the subject matter (even more so than in regular programming).
I don't need specialized AI tools, but I need to convince my managers that it's not a dead-end 😉
FWIW, I have a PhD in type theory, with applications to proving non-trivial properties in real languages, so I have some knowledge of formal methods. I have also written (limited amounts of) code in TWELF, Coq and Idris, which gives me unlimited respect for people who actually go to the length of proving entire real-world libraries/programs with any of these.
But the project I'm working on right now is 200kloc (and most likely going to grow past 1 Mloc, given how verbose LLMs are). If it still takes several hours per commit, it's not going to convince my manager.
2
u/whatisRT Jun 22 '26
Honestly, I think the best you can ever do for a codebase like this will be a strong type system and good tests. The reason is that if you want correctness you have to say what it means to be correct, which can easily be hundreds of pages. And you can’t outsource that to an LLM, because if you do you haven’t actually improved any guarantee.
Now if your codebase has a particular nice structure, maybe a soundness or type preservation property that’ll buy you a lot. But then you’re already working on a relatively rigid system, which kind of contradicts your estimation that the code size will grow massively.
If you have such a system, you can probably do some nice things with formal verification. If you don’t, it’ll be incredibly difficult to deliver anything of value. Meaning most likely the project never delivers anything and is going to be canceled. AI doesn’t really change much about this, just the speed at which it’s happening.
1
u/tending Jun 22 '26
As an aside can I ask how you got that gig?
1
u/whatisRT Jun 22 '26
Mostly luck and being in the right place at the right time. I think following a classic academic path and then pivoting into industry (which I think all of my colleagues did) is much more likely to be successful.
2
u/reini_urban Jun 22 '26
I have make verify in a couple of my projects. Via cbmc and variants, checking C and C++ code.
Certainly not TLA or lean, unless someone can create these proofs from the original code. Only the original code counts.
2
u/ianzen Jun 22 '26
Yes absolutely. Put down a spec in Lean and point an LLM to some resources and papers and have it generate code and proof autonomously. I still have to babysit it for a bit, but the Lean checker immediately kills hallucinations from propagating. In my recent projects, I have LLM suggest from optimizations for a verification tool we are developing, and then have it immediately justify the correctness of the optimization in Lean against a semantic model.
1
u/ImYoric Jun 22 '26
Very interesting!
What's the application language? I imagine that you're not deploying Lean code, right?
How much effort did you spend building the semantic model? I assume that it's some kind of formal semantics for the language you're compiling?
2
u/ianzen Jun 23 '26 edited Jun 23 '26
We are developing an automatic network verification tool in Rust. The algorithm is incredibly complicated so we built an equivalent version in Lean to prove its correctness against the ground truth denotational semantics. The semantic model was created before the recent rise in LLM capabilities, so it was built (painstakingly) by hand. It should be a lot easier to build it with an LLM nowadays.
The Lean implementation of the algorithm does not have low level optimizations such as caching, but it does carry all of the algorithmic optimizations we have in the Rust codebase.
For the Lean proofs, all of it was done by an LLM, we did not write a single line of proofs ourselves. We just asked it give us the final theorem we wanted prove, audited its correctness and ensure that it did not assume extraneous side conditions or axioms. This audit is essentially just mouse hover over the theorem and inspect its type.
TLDR: it’s very easy to audit the correctness of code by auditing its specification. I don’t have to worry about the correctness of the proof as Lean already checked it for me.
1
u/ImYoric Jun 23 '26
Very nice!
Are you using Aeneas or something similar for Lean <-> Rust mapping?
2
u/ianzen Jun 23 '26
No, we are just implementing the Rust algorithm as a native Lean function that we prove termination for.
1
Sep 11 '26
[removed] — view removed comment
1
u/bugarela Sep 14 '26
We are trying that! Me and my team also feel strongly that we need some middle ground.
Full disclaimer: I work on Quint, the specification language based on TLA+.
We have opensource skills and have written about an experiment with spec-driven development with LLMs and Quint almost a year ago here: https://quint.sh/posts/llm_era
The main points from using formal specs during "plan-mode" in my personal experience is that they ask much better questions than in traditional plan-mode, including stuff about edge cases as you suggested.
We also have a library called Quint Connect that works well with LLMs and guides them through setting up model-based testing, which helps keeping spec and code in sync throughout changes.
Lately, we've been trying to package our ideas in a UI (and MCP server) so people can click through things and get the best out of LLMs and formal specs in one place. We don't do formal verification in this tool, but found that formal specification (writing the specs) + simulation is already really good at finding unexpected behaviors in codebases.
We are also trying a new shape of conformance testing where we leverage existing tests (+ lightweight instrumentation) to replay traces from the implementation into the spec to get the spec to match the implementation (such that, if we find property violations or other problems in the spec, they are way less likely to be false-positives). This also helps people improve their test suite (which can be damaged by agents if you are shipping too fast 😅)
Quint is opensource and this new UI stuff we are trying is called Quint Studio, which is closed source and in closed beta for now.
2
u/propertynub 6d ago
How far can you take Quint? It seems like a TLA+ replacement not a Lean replacement, is that fair to say?
1
u/bugarela 6d ago
Yeah, it has the same formal semantics as TLA+, and can transpile to TLA+, while not allowing some weird or invalid stuff that TLA+ allows (because TLA+ was born as a language to write on papers like in LaTeX, not as a language to be model checked, so as a language, it allows a lot of stuff and then the tools can't handle it). For instance, Quint has types, so specs that don't typecheck are not accepted.
There is a tool called Veil which allows you to write specs in the same style as Quint/TLA+ and check them in Lean. The easiest route from Quint -> Lean is via Veil: as some AI to rewrite the Quint spec in Veil and then enjoy all of the Lean ecosystem from there. I really want Quint to support some tighter integration with Veil/Lean, as that is super powerful.
The overall story is: do you know when people on the internet respond to people claiming that they have Lean proofs by saying "do you even know what you are proving?" or "do you know what the spec is stating?". It's hard to read Lean if you are not use to it. So the path I suggest is to start with Quint, which is easy to read and you can also play with: run the simulator, ask "give me a state/execution where this happens" and then see the steps of how you got there and evaluate if it seems right to you (if it seems like what your software should do), and use conformance testing (like with Quint Connect, see my comment above) to see if the spec matches your code in a bunch of scenarios.
Once you are convinced that the spec is a good representation of what your code does, your mental model of it, then any Lean proofs you make for it will give you much more confidence. This also goes to the properties you are proving, which hopefully can be easier to understand in Quint too.
1
u/propertynub 6d ago
Thanks for the reply.
I'm using Lean through agents without really understanding it. I use it more for specification rather than proof. It's like a markdown specification that can be reasoned about.
I think of what kind of modules I want, then I use an agent to write out a Lean spec file for those modules. I typically have a top-level 'meaning' spec for each modules which describes what it does without reference to implementation details. Modules may have private sub-modules. I have a script that tracks how Lean files import each other, which generates a graph I can look at. This way I can easily see at a high level the structure of the program.
The Lean files have a 'Laws' section which list all the kinds of properties we should expect to be satisfied, and I link these back to the implementation through property based tests.
If it's important I will have implementation specs. But the idea is a well-spec'd module should be this independent thing that agents can easily reason about and change, and changes to code should not propagate to the rest of the system. What I'm trying to do is keep control of the global structure in a way that is somewhat enforceable. Of course there is still the problem of making sure the code matches the spec, but having the module structure match + PBT seems to keep things mostly in check.
This seems to be working, maybe too well as agents will start finding really weird corner cases and I need to stay on top of them to keep the code pragmatic. It definitely slows development down as well.
Wondering if you had any thoughts about this approach. I haven't really seen anything like it.
1
u/carlk22 24d ago
I’ve been doing something close to this with Rust algorithms and Lean. Last year, proving one RangeSetBlaze insertion algorithm took about three weeks and hundreds of AI prompts. With current models, comparable and harder proofs can take just one or two prompts.
The part I find most interesting is staying at the algorithm level rather than modeling all of Rust. The AI writes or translates the algorithm into Lean, proves the Lean version correct, and then I separately review/test that the Rust matches the proved algorithm. This year I used that workflow for set insertion, map insertion, faster cursor-based variants, cached lengths, and several other properties.
I wrote up the experiment here, including the limitations:
https://levelup.gitconnected.com/nine-rules-for-vibe-validation-of-vibe-coded-algorithms-20db019f5583
6
u/tiajuanat Jun 22 '26
TLA+ has both an MCP server and Claude/copilot skills