Solidus: Formally Verifying a Compiler Using Automated Research

What it is

Solidus is Paradigm's pre-alpha formally verified Solidity-to-EVM compiler, implemented in Lean. The Yul-to-EVM backend is already built and proven; the Solidity-to-Yul frontend does not yet exist. The project ships with a formal Solidity semantics (solidity-lean, targeting Solidity 0.8.35) and an open-sourced Codex skill used to build the backend.

How it works

The backend proof establishes that every program the compiler emits has identical outputs to the input Yul program for all inputs, excluding EVM-specific details like gas and memory layout. The semantics model only the state of the individual contract being compiled, but the proof is parametric over all possible external worlds — it only requires that the same external call return the same result in both the source and compiled program, not that the two programs behave identically across every possible concrete external state. The backend forks Nethermind's Yul/EVM semantics and is comparable in approach to Powdr's yul-compiler.

The current proof guarantees soundness only; completeness and performance are verified heuristically against a holdout test suite, not proven.

Preconditions / Affected

Relevant to teams evaluating Solidity compiler trust assumptions or considering contributing to formal-verification tooling. The compiler is pre-alpha, unaudited, and not production-ready — not a drop-in replacement for solc.

What to do

Two contribution challenges are live:

• Spec Hunt: find divergences between solidity-lean's formal semantics and actual Solidity 0.8.35 behavior. Submit a Foundry-based proof-of-concept; an AI agent reviews it, merges a fix to solidity-lean, or escalates to human review.
• Compiler Optimization: shrink Yul-to-EVM backend bytecode size while preserving the existing correctness proof (the soundness theorem must still hold). Baseline gap stated: the compiler currently emits almost 3x the bytecode of solc on Paradigm's test suite.

Caveats

The page states it will likely be possible for submissions to exploit subtle gaps in the formal verification to game scoring or introduce undetected problems — this is an acknowledged, open risk, not a solved one. The Solidity formal semantics is explicitly expected to still contain undetected divergences from real solc behavior. No human wrote or read any of the backend code; architectural judgment calls (e.g., which spec edits were acceptable) still required human intervention rather than full automation.