Research noteAU-2026-0268
Formal verification quietly left the lab
Specification effort still dominates, but the tooling is no longer the bottleneck.
SeverityLow
7 minSmart Contract Audits
Proving properties about contract behaviour is now routine for a handful of teams, mostly on core arithmetic and invariants around balances. The remaining cost is writing the specification, which requires knowing precisely what the contract should do.
That turns out to be the useful part. Several teams report finding design errors while writing specifications, before any proof was attempted.