Formally Verifying a Compiler Using Automated Research
Agents can do extraordinary things through automated research loops. Communities of automated researchers can achieve even more through competitions, like the ones we host on Paradigm Puzzles. But how do we know that what they produce is correct?
Formal verification with languages like Lean turns out to be beautifully complementary to automated research. It can prove that an agent’s output correctly solved a presented problem, or that an optimized program preserves properties of an unoptimized one. While these proofs are incredibly tedious to construct, the solution is the same as the problem: automated research. You can automate the creation of Lean proofs using AI, thanks to increasingly capable models like GPT-5.6 and Claude Fable 5 and specialized tools like Aristotle. And they allow collaboration by untrusted contributors, since contributions can be proven correct.
We’re introducing Solidus: a collaborative automated research project to build a formally verified Solidity compiler in Lean. We are kicking off this project with two new optimization puzzles: one to pin down a frozen source semantics of the Solidity language, and the other to optimize the already-proven backend of the compiler (while preserving the proof).
The Solidus project already includes a full formally verified backend that compiles from Yul (the intermediate representation used by the Solidity compiler) to EVM, as well as a new proposed formal semantics for Solidity. We plan to use automated research to finalize the Solidity semantics, build the frontend of the compiler, and optimize the implementation to make it not only the most secure Solidity compiler, but also the most efficient.
Solidus has already been a major automated research undertaking. It took over 1,700 hours (~10 weeks) of total Codex /goal time, with extra-high effort, in fast mode (~$150,000 at API rates). But we think that is nothing compared to the improvements that could come from opening it up to public contribution.
This is a pre-alpha project. The code has not been audited and is not production-ready. And it will likely be possible for submissions to take advantage of subtle gaps in the formal verification to game the score or introduce undetected problems. But we hope that these challenges can pressure-test some of those gaps, and help pave the way for even more ambitious projects in the future.
Why Formally Verify a Compiler?
Compilers are an essential part of the modern computing toolchain, but they are complex and open-ended pieces of software that are very difficult to test exhaustively. Formal verification of compilers protects against compiler bugs, like the one that led to a $50+ million smart contract hack in July 2023. It also makes formal verification of individual programs easier, since it lets developers prove statements about a high-level structured language, rather than low-level bytecode.
But perhaps most importantly, it allows us to fully set automated research loose on improving trusted codebases like compilers. It can enable more collaboration on secure codebases, since contributions can come with a certificate that they satisfy the properties required. It also allows extremely aggressive, trustless optimization of the compiler. Lean-based projects can potentially be automatically optimized much more aggressively than normal projects.
What Is Solidus?
Solidus is a planned compiler from Solidity (the most popular smart contract language) to the EVM, implemented in Lean.
Lean is a language and proof assistant for formal verification. While it is best known for its application to math, it is also a powerful and increasingly popular language for formal verification of computer programs. We implemented our compiler itself in Lean, to make it even more amenable to formal verification.
Solidity is the most popular smart contract language, and the EVM (Ethereum Virtual Machine) is the most popular blockchain virtual machine (used by chains like Ethereum, Tempo, and Monad).
The backend of Solidus (a compiler from Solidity’s intermediate representation, Yul, to the EVM) is built and formally verified. We use a slightly modified fork of the Yul and EVM semantics created by Nethermind, and prove that every program produced by our compiler has identical outputs for all inputs as the Yul program given to it (other than EVM-specific details like gas and memory layout). Our semantics only model the state of the individual contract being compiled, but the compiler fully supports external calls—the proof is parametric over all possible external worlds, as long as they are deterministic. (This backend is similar to the yul-compiler project released recently by the Powdr team.)
The frontend for the compiler (from Solidity to Yul) is not yet built, in part because no formal semantics for Solidity exists. To begin to rectify that, we built a formal semantics for Solidity to act as a source language for the compiler. This semantics likely still has some gaps, and one of the goals of the Solidus challenges is to find those gaps and harden it.
How We Built Solidus
Solidus was only possible because LLMs are now strong enough to take on extremely heavy research and engineering projects. The star contributor was GPT-5.6 and Codex, but we also made significant use of Harmonic’s Aristotle for some of the most complex proofs, and used Claude Fable 5 for some of the final steps.
No human read or wrote a single line of code for Solidus, but it was still nowhere close to a fully automated effort. We don’t think agents are good enough yet to solve this kind of task with a single /goal loop, although we suspect they will be good enough soon—probably by the end of the year.
One reason is that the spec for the compiler had to evolve as part of the proving process; until we were deep into the proving process, it wasn’t clear exactly what statement we could or would be proving about the compiler. This required some human judgment about which spec edits were acceptable, and which would violate the spirit of the compiler. Outsourcing such judgment to agents tends to result in drift or reward-hacking.
Another reason is that some human creativity was required for some of the higher-level architecture of the proof. For example, agents burned days attempting to prove that the source and target programs would be equivalent in all possible states that a concrete external world could have, before we suggested pivoting to prove the claim (much stronger, but ironically, easier to prove) that they would be equivalent regardless of how the external world worked, as long as the same external call by each program returned the same result.
We’ve open-sourced the Codex skill we used to build the compiler backend.
The Solidus Challenges
We think that challenges are an ideal way to organize collective autoresearch projects like these. We created two challenges to start:
Spec Hunt: One tricky problem in formal verification is ensuring that the proven spec for the problem actually matches the desired behavior. Solidity is a complex language, with no formal specification other than the solc compiler.
We wrote solidity-lean as an attempted formal semantics of Solidity 0.8.35, but we expect there are still many undetected divergences in it. This challenge allows users to score points by finding these divergences and submitting a proof-of-concept for them. These divergences are automatically tested using Foundry, and then reviewed by an AI agent, which fixes it by merging a change to the solidity-lean repo (or escalating to human review if needed).
Compiler Optimization: Another problem with formally verified codebases produced by agents is that, by default, they might be less efficient than ordinary codebases. On our test suite, our Yul-to-EVM compiler currently produces programs with almost 3x as much bytecode as solc. But automated research excels at optimization, particularly when correctness is verifiable.
We created a challenge to optimize the Yul-to-EVM backend of the Solidus compiler. Submissions have to improve on the performance of the existing compiler, while proving the same theorem about its correctness. (Note that the current compiler only guarantees soundness; completeness and performance are currently verified heuristically with a holdout test suite.)
We hope these challenges will help advance the Solidus project, and also serve as a prototype for other productive automated research projects in the future!