A smart contract's formal spec, readable like high-level code, and provably tied to the raw EVM bytecode.
That is the new evm-smith experiment.
Here is the whole behavioural spec of a WETH contract that an auditor reads:
(More and full write-up below)
Jun 24, 2026 · 4:53 PM UTC
16
12
136
13,634
2/ `deposit` credits the caller by `msg.value` and touches nobody else, `withdraw` debits exactly x, unknown selectors revert. Plain pre and post conditions.
The 86 bytes of bytecode are separately proven to satisfy each line.
1
6
638
3/ The fun part: we spec what a compiler usually hides.
Function selector dispatch and ABI argument decoding never show up in Solidity source, the compiler emits them. With no compiler in the loop, we wrote those bytes ourselves and can state and prove what they mean.
1
4
548
4/ The readable surface is a tiny eDSL: a predicate for "a call to f", an `ensures` for "running it guarantees", and accessors like `balance[sender]` and `old balance[sender]`.
About 150 lines of definitions, no heavy metaprogramming. Easy to read or to change.
1
4
418
5/ Each function reads as a big-step over a selector under preconditions, basically a Hoare triple:
{withdraw call, funded, no reentrancy} run {caller debited by exactly x}
The instruction by instruction walk stays hidden inside the proof.
1
4
381
6/ Two one-line lemmas pin "the selector" and "the argument" to what the compiler actually emits: `shr(224, calldataload(0))` and `calldataload(4)`.
So the spec's selector and argument are, by construction, the ABI's. Solvency reads the same way.
1
6
522
7/ `Spec.lean` is a proof-free interface; a separate witness proves the bytecode obeys every field.
The readable file is what a human signs off on, and the proof makes it mean something.
Full post: leonardoalt.github.io/human-…
Reach out if you want to contribute!
12
518
