Formally Verifying a Compiler Using Automated Research (Solidus)

What it claims

Solidus is Paradigm's pre-alpha Lean project for a formally verified Solidity-to-EVM compiler. Its Yul-to-EVM backend is built and proven. Every compiled program has identical outputs to the input Yul program for all inputs, excluding EVM details such as gas and memory layout. The frontend (Solidity to Yul) does not exist yet, because Solidity has no formal semantics beyond the solc compiler. Paradigm wrote solidity-lean, a proposed formal semantics of Solidity 0.8.35, as the future source language. The backend currently emits almost 3x as much bytecode as solc on Paradigm's test suite.

How it works

The backend proof uses a slightly modified fork of Nethermind's Yul and EVM semantics. The semantics model only the state of the contract being compiled. External calls are still fully supported: the proof is parametric over all possible external worlds, provided they are deterministic. The page compares the backend to the yul-compiler project recently released by the Powdr team.

That external-world framing came from a human. Agents spent days trying to prove equivalence across every state a concrete external world could have. Paradigm then suggested proving equivalence under any external world, as long as the same external call returns the same result to both programs. That claim is stronger and turned out easier to prove.

Paradigm says no human read or wrote code, but humans had to judge which spec edits kept the "spirit of the compiler." According to Paradigm, leaving that judgement to agents led to drift or reward-hacking. Paradigm predicts a single /goal loop will handle this kind of task "probably by the end of the year."

How to use it

The Codex skill used to build the backend is open-sourced. Two challenges run on Paradigm Puzzles.

Spec Hunt scores points for divergences between solidity-lean and solc 0.8.35, each submitted with a proof-of-concept:

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

Compiler Optimization accepts changes to the Yul-to-EVM backend that improve on the existing compiler's performance while proving the same correctness theorem.

Limits

• The code is unaudited and not production-ready.
• Paradigm expects submissions may exploit subtle gaps in the verification to game scores or introduce undetected problems.
• Only soundness is proven. Completeness and performance are checked heuristically against a holdout test suite.
• The proof assumes deterministic external worlds and ignores gas and memory layout, so gas behaviour is outside the guarantee.
• solidity-lean "likely still has some gaps," which Spec Hunt is meant to find.

The page names no repository URLs, licence or install commands.