For Solidity builders, a compiler must turn contract code into executable instructions without changing its intended behavior. Paradigm’s Solidus project aims to make that translation formally verifiable—and to let automated researchers improve the compiler while preserving its correctness proof.
In its article published on July 24, 2026, at 23:00 UTC+8, Paradigm introduced Solidus as a collaborative research project implemented in Lean, a programming language and proof assistant. The project already has a formally verified backend that translates Yul, an intermediate representation used by the Solidity compiler, into code for the Ethereum Virtual Machine (EVM). The Solidity-to-Yul frontend is not yet built.
Solidus is pre-alpha, unaudited and not production-ready. Paradigm also warns that contributors may be able to exploit gaps in the formal verification to manipulate challenge scores or introduce undetected problems.
What the backend proves—and what it does not
According to Paradigm, the backend’s proof establishes that compiled programs produce identical outputs to their input Yul programs for all inputs, excluding EVM-specific details such as gas and memory layout. It uses a slightly modified fork of Yul and EVM semantics developed by Nethermind. Here, semantics means a precise description of how a language’s programs behave.
The model covers the state of the individual contract being compiled. External calls are supported: the proof applies across possible external worlds, provided they are deterministic. Paradigm describes a key proof-design decision as requiring the same external call from each program to return the same result, rather than attempting to enumerate every state of a concrete external world.
The current compiler guarantees soundness. Completeness and performance are checked heuristically using a held-out test suite, rather than established by the same formal guarantee. These boundaries matter: a proof establishes a specified property under its assumptions, not the absence of every possible problem.
Paradigm points to a compiler bug linked to a smart-contract hack of more than $50 million in July 2023 as motivation for this work. It also argues that a verified compiler can make contract-level verification easier by allowing developers to reason about high-level code rather than only low-level bytecode.
Two challenges target the specification and the compiler
Spec Hunt: find mismatches in Solidity behavior
Paradigm created solidity-lean, an attempted formal semantics for Solidity 0.8.35, as a proposed source language for the future compiler frontend. The team expects it still contains undetected differences from Solidity’s behavior as implemented by solc.
The Spec Hunt challenge awards points for identifying those differences and submitting proofs of concept. Submissions are automatically tested using Foundry, then reviewed by an AI agent. The agent fixes accepted discrepancies through changes to the solidity-lean repository or escalates them for human review when needed.
The task addresses a fundamental limitation of verification: proving that software follows a specification is only useful if the specification captures the intended behavior.
Compiler Optimization: improve output while preserving the proof
On Paradigm’s test suite, the current Yul-to-EVM backend produces programs with almost three times as much bytecode as solc.
The optimization challenge asks contributors to improve the existing compiler’s performance while proving the same correctness theorem. The aim is to make aggressive optimization possible without abandoning the property already established by the proof. Paradigm’s ambition to build a highly secure and efficient Solidity compiler remains a project goal, not a demonstrated result.
AI-generated code still required human direction
Paradigm reports that building Solidus took more than 1,700 hours—about 10 weeks—of total Codex /goal time, using extra-high effort in fast mode, equivalent to roughly $150,000 at API rates.
The team identifies GPT-5.6 and Codex as the main contributors, with Harmonic’s Aristotle used for some of the most complex proofs and Claude Fable 5 used during some final steps. It says no human read or wrote a line of Solidus code.
That does not mean the effort was fully autonomous. Humans judged which changes to the evolving specification were acceptable and helped shape the proof architecture. Paradigm says delegating specification judgments to agents tended to produce drift or reward-hacking. The team also open-sourced the Codex skill used to build the backend.
For builders assessing the announcement, the distinction is straightforward: Solidus has a formally verified Yul-to-EVM backend, not a completed, production-ready Solidity compiler. Its public challenges are intended to strengthen the proposed Solidity semantics and improve backend efficiency while pressure-testing the verification itself.
Original article: “Formally Verifying a Compiler Using Automated Research,” Paradigm