Formal Verification in the Age of AI

Duration: NaN:NaN:NaN

Speaker: Fricoben

Type: Lightning Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

AI is rapidly changing how smart contracts are designed and shipped. It accelerates implementation, but also expands the volume, complexity, and attack surface of code deployed onchain. Reviews, fuzzing, and test suites remain valuable but sample behavior; they cannot establish that critical properties hold in every reachable state. This talk introduces formal verification: translating protocol intent into properties—solvency, access control, conservation of value, and liquidation accounting—and proving them across a model of contract behavior. It distinguishes a proof's guarantees from its assumptions. We then examine where AI fits: reading code, proposing specifications, constructing models, and accelerating proof development. AI is not trusted; Lean mechanically checks the completed proof. Attendees leave with a practical model for how AI can make maintained, machine-checked security specifications feasible—and why providers will be judged by guarantees they own.