Using LLM Generated Formal Specs to Prevent the Next DeFi Hack | Mooly Sagiv (Certora) at ETHConf

Sun, Aug 2, 2026, 12:00 AM

In this talk, Mooly Sagiv from Certora presents how LLM generated formal specifications can help prevent the next DeFi hack. He frames the problem: coding agents are increasingly replacing software engineers, but hackers are winning, and even with excellent auditing firms and tooling the industry cannot find all bugs. The situation will worsen as every new AI model release creates new threats while code grows more complex. He critiques the informal approach to intent taken by companies like Anthropic, arguing intent should not be handled informally, and proposes agentic formal verification as the solution. He pushes back on the myth that formal verification is intractable or requires a PhD, arguing the real hard problem is not computation but formal specification: verification is only as good as the properties you specify, which is why teams that claim to be formally verified still get hacked, since they verified the wrong property. Mooly explains Certora's new open source, token based tool that bridges the gap between informal and formal specs. A developer writes intent informally (for example keep the balance safe), and the tool automatically generates a formal invariant (the sum of balances equals the total), which can then be proven or tested. The tool is agnostic to Certora's own prover, works with tools like Rocq, Lean, and Halmos, and fits into the development cycle before an audit through an interactive human-in-the-loop process, including a design hardening agent that makes designs more verification ready from the design document stage. He demos a toy counter contract with a trivial bug, showing how the tool generates properties in English, proves two of three rules, surfaces the bug, and validates the fix with a mathematical guarantee that future LLM versions cannot break. He then shows a real anonymized gambling protocol audited before deployment, where the tool automatically inferred 15 properties, found a real violation confirmed by their team, and suggested a validated fix. He closes on the product launching July 15 (Solidity only, GPL3, generating Foundry tests and including static analysis and bug finding at around $300 per run), and two takeaways: AI is why formal verification finally matters, and AI is also what makes formal verification easy by translating prover output into human understandable explanations. 00:00 Introduction 00:56 A Talk for Coders and Non-Coders Alike 01:18 How Coding Agents Are Replacing Software 01:47 Why Auditing and Tools Cannot Find All Bugs 02:28 Why Informal Intent Is the Wrong Approach 02:40 Introducing Agentic Formal Verification 03:05 Making Formal Verification as Easy as Testing 03:29 A History of Formal Verification and Its Myths 04:01 Why Intractability Is a Myth 04:32 Why Verification Depends on Specification 04:52 Why Verified Code Still Gets Hacked 05:11 How LLMs Help Find Formal Specifications 05:29 From Intent to Invariant 06:35 Beyond Verification: Generating Tests 07:07 How It Fits Into the Development Cycle 07:30 A Tool to Use Before the Audit 07:59 Why Getting Properties Right Is Hardest 08:37 Inside the Tool: Agnostic to the Prover 09:30 Hardening the Design for Verification 10:06 The Audit Agent and Security Review 10:44 Plugging In Rocq, Lean, and Halmos 11:01 Two Examples: Toy and Real 11:34 The Toy Counter Contract Bug 11:55 How the Agent Finds Properties in English 12:34 Proving Rules and Surfacing the Bug 12:57 Why a Violation Could Be Code or Spec 13:30 Validating the Fix With a Proof 14:26 Applying the Tool to Real Code 14:45 A Real Protocol Audited Before Deployment 15:20 How the Tool Inferred 15 Properties 16:25 The Paused Contract Condition It Caught 17:00 Finding and Confirming a Real Bug 17:33 Validating the Suggested Fix 18:04 The Status of the Tool 18:49 The July 15 Product Launch 19:40 Pricing Around $300 per Run 20:19 Two Surprising Takeaways 20:47 Why AI Made Formal Verification Matter 21:06 How AI Makes Formal Verification Easy 22:33 Closing and Call to Try the Tool _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ *ETHConf 2026* ETHConf is a 3 day event for founders, industry leaders, and builders who are excited about the possibilities of building on top of Ethereum. Connect with 2,000+ top innovators in crypto, finance, technology, and policy at our inaugural three-day event packed with showcases, demos, partnerships, and conversations shaping the future of the global economy. _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ✅ *Follow ETHConf* X: https://x.com/ethconf Website: https://ethconf.com _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 🎟️ Get your early bird tickets for ETHConf 2027: https://ethconf.com/2027#tickets 🎤 View the full ETHConf 2026 Speaker Schedule: https://ethconf.com/schedule _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _