Harnessing LLMs to generate secure code

About this session

Mooly Sagiv opened by challenging a common assumption: that large language models make smart contract code less secure. He argued the opposite could hold if a model's output was checked against a formal specification rather than trusted on its own. Presenting with his Certora colleague John Toman, he introduced an internal tool, previously called VeriSafe and now called Composer, that generated a contract implementation from a spec and used a formal-verification prover to check it, feeding failures back to the model until the code satisfied that spec.

Sagiv framed the problem first. Contract security already leans on skilled developers plus auditing, fuzzing and formal verification, and bugs still get through. The common prediction was that models would make this worse by producing more buggy code, faster. His counter drew on an older idea, starting from a specification rather than from code, paired with a model: the model proposed implementations, and formal verification caught the ones that were wrong.

Toman walked through the mechanism on a contrived liquidity pool where withdrawal fees rose with size. A design document and a formal specification went in alongside an interface, and before generating code the model first scanned the documents for requirements the formal rules didn't cover. It produced an implementation, checked by Certora's prover at the bytecode level; a failure returned a counterexample, fed back to the model for another pass. The model could also flag the spec as wrong when a counterexample conflicted with the design intent, and it would then propose a change that a human had to approve.

Their demo's first implementation blocked one large withdrawal but not the same amount split into many small ones, a gap in the spec rather than a prover failure. Instead of restarting, the team added a rule and fed the prior implementation back in to keep the fix minimal. That gap also marked the edge of what the tool actually proved: the final code was checked against the current formal specification, not against every possible flaw, so an incomplete spec could still let a bug through. In the Q&A, the team said the loop itself carried no formal guarantee of converging, only a model prompted to ask for help when stuck, with a person able to interrupt it. They placed the technique inside an older synthesis idea, generate and check until it holds, with a language model as the proposer.