Using LLM Generated Formal Specs to Prevent the Next DeFi Hack
summary
LLM-generated specs convert informal intent into formal invariants (for example sum of balances equals the total) that feed provers like Certora’s, Rocq, Lean and Halmos and produce provable guarantees. A toy counter demo shows the agent generates three rules, proves two and surfaces the one bug; an anonymized gambling protocol auto-infers 15 properties, finds a paused-condition violation and suggests a validated fix. Product launches July 15, Solidity GPL3, generates Foundry tests and costs about $300 per run.
AI-written summary · about
chapters (40)
- 0:00Introduction
- 0:56A Talk for Coders and Non-Coders Alike
- 1:18How Coding Agents Are Replacing Software
- 1:47Why Auditing and Tools Cannot Find All Bugs
- 2:28Why Informal Intent Is the Wrong Approach
- 2:40Introducing Agentic Formal Verification
- 3:05Making Formal Verification as Easy as Testing
- 3:29A History of Formal Verification and Its Myths
- 4:01Why Intractability Is a Myth
- 4:32Why Verification Depends on Specification
- 4:52Why Verified Code Still Gets Hacked
- 5:11How LLMs Help Find Formal Specifications
- 5:29From Intent to Invariant
- 6:35Beyond Verification: Generating Tests
- 7:07How It Fits Into the Development Cycle
- 7:30A Tool to Use Before the Audit
- 7:59Why Getting Properties Right Is Hardest
- 8:37Inside the Tool: Agnostic to the Prover
- 9:30Hardening the Design for Verification
- 10:06The Audit Agent and Security Review
- 10:44Plugging In Rocq, Lean, and Halmos
- 11:01Two Examples: Toy and Real
- 11:34The Toy Counter Contract Bug
- 11:55How the Agent Finds Properties in English
- 12:34Proving Rules and Surfacing the Bug
- 12:57Why a Violation Could Be Code or Spec
- 13:30Validating the Fix With a Proof
- 14:26Applying the Tool to Real Code
- 14:45A Real Protocol Audited Before Deployment
- 15:20How the Tool Inferred 15 Properties
- 16:25The Paused Contract Condition It Caught
- 17:00Finding and Confirming a Real Bug
- 17:33Validating the Suggested Fix
- 18:04The Status of the Tool
- 18:49The July 15 Product Launch
- 19:40Pricing Around $300 per Run
- 20:19Two Surprising Takeaways
- 20:47Why AI Made Formal Verification Matter
- 21:06How AI Makes Formal Verification Easy
- 22:33Closing and Call to Try the Tool
related talks
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
25mVerifying LLM powered Code Transformations with Equivalence Checking
16mPreventing Hacks with Security Rules Written in Solidity
01h 00mAI Safety through Programming?
47mHarnessing LLMs for Next-Level Security Analysis
27mThe Lean LLM development playbook
01h 00mFrom LLM Theory to Practical Agentic Implementations
32mThe Sorcerer’s Apprentice: The craft of building reliable solutions with LLMs