Paradigm’s Solidus project aims to build a formally verified Solidity-to-EVM compiler in Lean, using AI-assisted research and public optimization challenges. The important distinction for developers: its Yul-to-EVM backend is built and formally verified, but the Solidity-to-Yul frontend is not yet implemented.
Source publication time: July 24, 2026, at 23:00 UTC+08:00. This article summarizes that announcement, not a subsequent release.
Status at publication: Solidus was pre-alpha, unaudited and not production-ready. Paradigm warned that submissions could exploit subtle gaps in the formal verification to manipulate scores or introduce undetected problems.
What the backend actually proves
Solidus is implemented in Lean, a programming language and proof assistant. Its existing backend translates Yul—the intermediate representation used by the Solidity compiler—into EVM programs.
Using a slightly modified fork of Nethermind’s Yul and EVM semantics, Paradigm says it proves that each compiled program produces the same outputs for all inputs as its Yul source, apart from EVM-specific details such as gas and memory layout.
That claim has important boundaries:
- The semantics model the state of the individual contract being compiled.
- External calls are supported. The proof is parametric over possible external worlds, provided they are deterministic.
- The compiler currently guarantees soundness; completeness and performance are checked heuristically using a holdout test suite.
A proof therefore needs to be read alongside its specification and assumptions. It is not a blanket guarantee that the entire project is ready for production.
Why the Solidity frontend is still missing
The announcement describes Solidity as lacking a formal specification other than the behavior of the solc compiler. To provide a source-language definition for Solidus, Paradigm developed solidity-lean, an attempted formal semantics for Solidity 0.8.35.
Paradigm expects that definition still contains undetected divergences from Solidity’s behavior. Finding and correcting those differences is one of the project’s initial tasks, before completing the frontend and optimizing the compiler.
The broader motivation is to make compiler changes easier to verify. Paradigm points to a compiler bug behind a $50+ million smart-contract hack in July 2023 as an example of the risk. A verified compiler can also help developers reason about high-level programs rather than proving properties directly about low-level bytecode.
Two challenges for contributors
1. Spec Hunt: find mismatches in the language definition
Participants can earn points by identifying divergences in solidity-lean and submitting proof-of-concept examples.
The documented review process is:
- Foundry automatically tests the reported divergence.
- An AI agent reviews it.
- The agent fixes it by merging a repository change, or escalates it for human review when needed.
The intended outcome is a better-aligned formal definition of Solidity—not a claim that the existing definition is already complete.
2. Compiler Optimization: improve the backend without losing the proof
On Paradigm’s test suite, the Solidus backend produced programs with almost three times as much bytecode as solc at publication.
Optimization submissions must improve compiler performance while proving the same correctness theorem. The challenge is designed to let contributors change the implementation aggressively without abandoning its established proof obligations.
AI-generated code still required human judgment
Paradigm reports more than 1,700 hours—approximately 10 weeks—of total Codex /goal time, using extra-high effort in fast mode, equivalent to approximately $150,000 at API rates.
It names GPT-5.6 and Codex as the main contributors, Harmonic’s Aristotle for some complex proofs, and Claude Fable 5 for some final steps. Paradigm also says it open-sourced the Codex skill used to build the backend.
Although Paradigm says no human read or wrote a line of Solidus code, it explicitly describes the work as far from fully automated. Humans judged whether evolving specifications remained faithful to the compiler’s intended behavior and helped redirect the proof architecture when agents stalled.
For developers evaluating Solidus, the practical takeaway is to distinguish the verified backend from the unfinished full compiler, and the proven theorem from properties still checked through testing. The public challenges are intended to pressure-test those boundaries, not to establish production readiness.
Original article: “Formally Verifying a Compiler Using Automated Research” — Paradigm