On day one of Devcon India 2026, Certora’s Mooly Sagiv joined Ethereum co-founder Vitalik Buterin, Fredrik Svantes of the Ethereum Foundation, and Josselin Feist of Aave for Ethereum Security in the Age of AI, a panel moderated by 0xRajeev. Drawing on Certora’s work with Aave V4, Sagiv explained why formal verification should begin while a DeFi protocol is still being designed and how developers can use large language models (LLMs) to turn intended behavior into rules they can check.

Below, we recap Sagiv’s main points, from the order in which teams write specifications and smart contract code to a question he wants more DeFi protocols to ask: if a security assumption fails, how much could users lose? Click here to watch the full Devcon India panel.

Why formal verification started early in Aave V4

When 0xRajeev asked how DeFi protocols should use LLMs for formal verification, Sagiv began with two decisions that come before choosing a tool. The first is how to divide the protocol into modules. The second is when to start checking what those modules are supposed to do.

Certora has worked with Aave since V1. What stood out to Sagiv about Aave V4 was that Aave’s engineers were already thinking about modularity before they spoke to Certora. That gave the teams an opportunity to question assumptions while they could still change the architecture. The collaboration included early design reviews, threat modeling, and continuous formal verification as development progressed. For a concrete example, the Aave V4 Hub report documents the specification Certora checked against the Hub implementation using the Certora Prover. 

Sagiv saw an opportunity for smaller DeFi teams as well. Even with a limited audit budget, developers can use an LLM alongside verification tools to start writing and checking properties during development. Watch Sagiv discuss Aave V4 and modular design at 20:19.

How can an LLM help verify a smart contract before the code is written?

Feist described an emerging development workflow in which an engineer writes an informal specification and asks an LLM to generate smart contract code. Sagiv added an intermediate step that Certora had used in its Aave V4 work: ask the model to generate a formal specification before it generates the implementation.

A formal specification expresses intended behavior precisely enough for a verification tool to check whether the code satisfies it. Writing that rule first gives the engineer a chance to ask whether it captures what the protocol designer meant. It also gives the model a more precise target when it generates code. Sagiv said that, in his team’s experience, this sequence helped reduce hallucinations and could produce code that was easier to verify.

Feist’s follow-up explains why reviewing the rule matters. A tool can reason correctly about a specification that describes the wrong behavior. The earlier a team puts its assumptions into a form that engineers can inspect, the earlier it can catch that mismatch. Watch Feist and Sagiv discuss specification-driven development at 25:51.

Which DeFi security properties are worth proving?

Sagiv’s concern about Ethereum’s security priorities grew out of his academic career. He recalled moving from paper to paper while colleagues in Australia concentrated on a single verification project and took it much further. He saw a similar risk in pursuing many languages, tools, and properties at once. Choosing a concrete goal, such as securing a wallet end to end, gives researchers a basis for deciding where more testing and verification would make a difference to users. Watch Sagiv discuss Ethereum security priorities at 9:40.

His clearest DeFi example was a protocol that lists a bad asset. The contracts might behave exactly as specified, yet the listing decision can still expose users to losses. Sagiv compared the protection he would like to see to an elevator’s safety mechanism. Even if a component fails, the mechanism can slow the descent. What assurance could a lending protocol offer after one of its own assumptions fails?

One answer would be a demonstrable upper bound on losses under a defined failure scenario. That would tell users something concrete about their exposure at the moment it matters most. Sagiv presented this as a goal for future work. Watch Sagiv explain the elevator analogy at 30:49.

What do engineers catch that AI agents miss?

Late in the panel, Feist described missing a bug after relying too heavily on AI during a code review. His advice to researchers was to explain their own understanding of a component to the model and ask it to challenge their reasoning. Sagiv then shared a related exercise from Certora: an engineer and an agent each write a specification or rule, then compare what they found.

Sometimes the engineer catches a bug the agent missed. Sometimes the agent writes a rule that exposes a case the engineer overlooked. When the rules differ, the engineer has a concrete question to investigate: what behavior does one rule allow that the other rules out, and which one reflects the protocol’s intent? For a small team deciding who owns security, that judgment is an important part of the job. Watch Feist and Sagiv discuss AI-assisted security reviews at 50:26.

Conclusion

For a team building a DeFi protocol, Sagiv’s advice suggests a practical starting point: choose one consequential promise the protocol makes to users and write it down while the design is still open. Ask an engineer and an LLM to express that promise as a formal rule. Where their versions differ, take the question back to the people who designed the protocol before checking the implementation.

That sequence connects the Aave V4 experience to Sagiv’s broader point about Ethereum security. AI can help teams write specifications earlier and explore cases an engineer might miss. The decision that gives that work value is choosing what users should be able to count on, especially when something goes wrong.

New to formal verification? Learn what a formal specification is and how developers use it to check whether a smart contract behaves as intended. Read Certora’s guide to formal verification.