Formally Verifying a Compiler Using Automated Research (Solidus)

What it is

Solidus is a Lean project from Paradigm to build a formally verified Solidity-to-EVM compiler. Only the Yul-to-EVM backend exists, together with a draft formal semantics of Solidity 0.8.35 called solidity-lean. The Solidity-to-Yul frontend is not built. Paradigm calls the project pre-alpha, unaudited and not production-ready.

How it works

The backend builds on a slightly modified fork of Nethermind's Yul and EVM semantics. The proven theorem says every compiled program has the same outputs as the source Yul program for all inputs, apart from EVM details such as gas and memory layout.

The semantics model only the state of the contract being compiled. External calls are still fully supported, because the proof is parametric over every external world, provided it is deterministic. Equivalence holds whenever the same external call returns the same result in both programs. Paradigm says agents spent days trying to prove equivalence over all states of a concrete external world. Proving the stronger parametric claim was easier.

Paradigm reports the build took over 1,700 hours (about 10 weeks) of Codex /goal time at extra-high effort in fast mode, about $150,000 at API rates. It credits GPT-5.6 with Codex as the main contributor, Harmonic's Aristotle for the hardest proofs, and Claude Fable 5 for some final steps. It says no human read or wrote the code, but humans had to decide which spec edits were acceptable, since the provable statement changed during proving. It has open-sourced the Codex skill used for the backend.

What to do

Two Paradigm Puzzles challenges are open:

• Spec Hunt: find divergences between solidity-lean and real Solidity behavior and submit a proof-of-concept. Foundry tests each one automatically. An AI agent then reviews it and merges a fix into the solidity-lean repo, or escalates to a human.
• Compiler Optimization: improve the Yul-to-EVM backend while proving the same correctness theorem. The compiler currently emits almost 3x the bytecode of solc on Paradigm's test suite.

Caveats

• Paradigm expects submissions may exploit subtle gaps in the verification to game the score or introduce undetected problems. Part of the aim is to pressure-test those gaps.
• The compiler guarantees only soundness. Completeness and performance are checked heuristically against a holdout test suite, not proven.
• The Solidity semantics likely has gaps. No formal Solidity specification exists other than the solc compiler.
• The page gives no scoring rules, deadlines or prizes for either challenge.