Don't Review the Code: Formal Specs First Smart Contract Development
2026-11-05 –, Lotus Stage 2

AI can generate a plausible implementation of anything, which moves the bottleneck from writing code to knowing it's correct. A working pipeline — behavioural specs, synthesised Yul, machine-checked refinement — and why the only component you have to trust is the checker.


AI can now produce a plausible implementation of almost anything. That moves the bottleneck from writing code to knowing whether it's right, and the answer isn't more code review — it's making the specification the artifact humans own, and reducing the trusted component to a single deterministic checker.

I'll walk through a working pipeline: high-level behavioural specs in Act, AI-generated Yul, and machine-checked refinement between the two. The running example is a fully onchain orderbook, where designing for verifiability changed the architecture itself — custody that proves solvency without trusting its callers, and units chosen so that no division exists anywhere in the protocol.

I'll also cover what doesn't work yet: storage-layout abstraction, matching loops, and the uncomfortable fact that a specification can prove instantly because it says nothing at all.

Protocol Engineering Team Lead @ Monad Foundation
ex co-founder in DeFi
ex Ethereum Foundation (core solidity compiler team)