Harnessing LLMs to generate secure code | Mooly Sagiv and John Toman
Duration: 00:21:54
Speaker:
Type: Talk
Expertise:
Event: Devcon
Date: Jul 2026
Prev. title: VeriSafe: Spec-Driven Smart Contract Development Technology
Despite significant progress in Web3 security, smart contract vulnerabilities remain extremely challenging for both humans and machines to detect. One reason for this is that smart contract vulnerabilities are particular to the protocol functionality and its unique implementation.
In addition, static analysis and AI tools often produce numerous false positives and can overlook many critical errors. As a result, sometimes bugs are exploited several years after deployment.
At Agentic Zero, Mooly Sagiv (Co-Founder & Chief Scientist, Certora) and John Toman (Senior Technical Fellow, Certora) describe a new approach for developing smart contracts, starting from libraries to complex code. The main idea is to start with an informal and declarative specifications and then utilize LLMs and formal verification to derive a smart contract that implements the required specification. The derived contract is guaranteed to be formally verified. The formal specification and code are audited to confirm that the code is safe.
This code-generation platform technology is available as an open-source.
