Solidus: Formally Verifying a Compiler Using Automated Research

What it claims

Paradigm has a Lean-implemented Yul-to-EVM compiler backend with a machine-checked proof. Every bytecode program it emits produces the same outputs, for all inputs, as the source Yul program. Gas and memory layout are excluded from that guarantee. Alongside it is a proposed formal semantics for Solidity 0.8.35 called solidity-lean. The Solidity-to-Yul frontend does not exist yet. The build used over 1,700 hours (about 10 weeks) of Codex /goal time on extra-high effort in fast mode, roughly $150,000 at API rates. No human wrote or read the code.

How it works

• Semantics base: a slightly modified fork of Nethermind's Yul and EVM semantics.
• Scope of the model: only the state of the contract being compiled is modelled. External calls are still fully supported because the proof is parametric over every possible external world, provided that world is deterministic.
• The decisive proof pivot: agents spent days trying to prove equivalence across all states a concrete external world could have. A human then redirected them to a stronger claim that turned out easier to prove: the two programs are equivalent however the external world behaves, as long as the same external call returns the same result in each program.
• Where humans were still needed:
• The spec had to change during proving, and a human judged which edits kept the "spirit of the compiler." The authors report that leaving this judgment to agents led to drift or reward-hacking.
• Some proof architecture needed human input, such as the pivot above.
• Tools: GPT-5.6 via Codex did most of the work. Harmonic's Aristotle handled some of the hardest proofs, and Claude Fable 5 handled some final steps. The Codex skill used to build the backend is open-sourced.
• Comparable work: the authors call the backend similar to Powdr's recently released yul-compiler.

Evidence

On Paradigm's test suite, the verified backend emits almost 3× the bytecode of solc. Correctness is proven, but output efficiency is far behind the production compiler. The stated motivation is compiler bugs such as the one behind a $50M+ smart-contract hack in July 2023.

How to use it (the challenges)

Both challenges run on Paradigm Puzzles.

Spec Hunt pays points for finding divergences between solidity-lean and real Solidity 0.8.35 behaviour. Submissions are handled like this:

flowchart LR
  A[Divergence PoC] --> B[Foundry auto-test]
  B --> C[AI agent review]
  C -->|fixable| D[Merge fix to solidity-lean]
  C -->|unclear| E[Human review]

Compiler Optimization asks for improvements to the Yul-to-EVM backend's output that still prove the same correctness theorem.

Limits

• Status: pre-alpha, unaudited, and not production-ready.
• Soundness only: completeness and performance are checked heuristically against a holdout test suite, not proven.
• Known proof gaps: the authors expect submissions may exploit subtle gaps in the formal verification to game scores or slip in undetected problems.
• Narrow guarantee: gas and memory layout are outside it, and the external world must be deterministic.
• Unvalidated semantics: the Solidity semantics is expected to diverge from solc in many places. No Solidity formal spec exists beyond solc itself.
• Not fully automated: the authors say one agent loop cannot yet do this end to end and expect that to change "probably by the end of the year." That is a forecast, not a result.