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

- Speakers: [Mooly Sagiv](https://streameth.org/speakers/mooly-sagiv)
- Channel: [ETHGlobal](https://streameth.org/ethglobal)
- Date: 2026-07-09
- Duration: 22:51
- Topics: Certora, Mooly Sagiv, ETHConf, formal verification, formal specification, LLM, DeFi hacks, smart contract security, agentic formal verification, invariants, provers, auditing, security research, Solidity, CVL, Rocq, Lean, Halmos, static analysis, bug finding, design hardening, human in the loop, intent, coding agents, AI security, open source, GPL3, Foundry, testing, vulnerabilities, exploits, blockchain, Ethereum, RV4, mathematical proof, deployment, properties
- Watch: https://streameth.org/watch/yt-lpx5ulFyCL8
- YouTube: https://www.youtube.com/watch?v=lpx5ulFyCL8

## Description

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

_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _