We are releasing Solidity Spec, an open-source research preview of an executable formal model of Solidity in Lean. The repository is available at okcontract/solidity-spec, alongside a paper describing its semantics and machine-checked proofs for explicitly defined parts of the model. The current profile targets Solidity 0.8.36 and the Cancun EVM on Lean 4.29.0.
This work grows out of oksolc. Building and verifying a compiler requires a precise account of the behavior it must preserve. We developed these semantics alongside our compiler certificate models before extracting them into a standalone package so researchers can inspect, execute, and extend the model independently. Building the Lean package requires neither Zig nor a Python frontend, and it has no external Lean dependencies.
Because the model is executable, we can both run concrete examples and prove properties in Lean about machine transitions, state invariants, and source-to-target agreement. To ensure the definitions actually match Solidity, we test them against the language reference and real compiler runs.
Consider two memory references, a and b, pointing to the same one-element
uint256[], initially containing 1, in the following expression:
(a[0] = 2) + b[0]
Reading through b before the assignment gives 3; reading afterward gives
4. Solidity leaves the evaluation order of ordinary subexpressions unspecified
while preserving statement order and Boolean short-circuiting. A compiled
artifact picks one order, so a source model has to account for all permitted
choices. Solidity Spec exposes those choices at each expression group and models
the shared physical memory cell. Solidity's evaluation-order
reference
describes the language boundary behind this example.
Calls, conversions, and failures complicate this further. Internal helpers can write through aliases, one argument can mutate state read by another, and a subsequent revert has to restore the call checkpoint. The model handles captured locations, copies, internal call frames, and rollbacks within a single execution machine. It also distinguishes Solidity panics and reverts from unsupported behavior or host fuel exhaustion, ensuring out-of-fuel runs are never mistaken for valid source results.
The main safety theorem connects static checks on resolved syntax to an invariant over local values, physical heap contents, function handles, and saved continuations. Given a valid initial state and a closed, checked function table in the supported profile, any finite execution with enough fuel either preserves that invariant or yields a valid source outcome across all permitted evaluation orders. Source failures roll back to the checkpoint. The profile covers scalar operations, canonical memory word arrays and aliases, scalar persistent and transient storage, structured control flow, and closed internal calls (including recursion). Host fuel is tracked conservatively and kept separate from EVM gas, so the theorem holds without assuming termination.
Formal Solidity semantics have a substantial history. Executable semantics in K and the Coq-based Lolisa appeared in 2018. Isabelle/Solidity provides executable semantics and program proofs, while Lean developments include SolidCore and SolidiKeY. Solidity Spec brings together non-deterministic expression order, physical memory aliasing, call rollback, scoped machine safety, and a quantified source-to-target proof in one model.
This release does not formalize all of Solidity. The execution machine takes typed syntax trees with declarations and function references already resolved, leaving source parsing and elaboration outside the verified boundary. The safety theorem also covers a narrower subset than the full set of operations the machine can execute. Arbitrary external calls, inline assembly, full ABI encoding, and end-to-end compiler preservation remain future work. The paper details these boundaries and the development history.
You can check the standalone package from a Solidity Spec checkout with the pinned Lean toolchain:
make replay
make replay builds the libraries and regression modules, then rechecks the
foundation, pilot, and scalar machine proof closures from scratch.
Execution clients can import Solidity.Execution. Additional lemmas live in
Solidity.Execution.Proofs, and the admitted-state safety theorems are in
Solidity.Execution.Safety. The top-level Solidity import retains
compatibility interfaces for existing proof clients. Earlier integration audits
and compiler experiments used internal oksolc harnesses not included in this
release; the paper separates those internal runs from the standalone checks
reproducible in this repo.
We welcome counterexamples, comparisons, and external proof clients that test these interfaces. Next, we plan to support direct Solidity source ingestion, stronger composition theorems, and larger compiler preservation proofs. The code, proofs, and paper are available at okcontract/solidity-spec.