Don't Review the Code: Formal Specs First Smart Contract Development

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.

Speakers: Dorde Mijovic

Track: Users, Builders, and Agents