Trail of Bits used six months of agent-built tooling to catch a fund-draining bug before the audit began

Trail of Bits spent six months preparing to audit the Miden zkVM, a zero-knowledge virtual machine written in a custom assembly language with almost no existing developer tooling. Rather than pointing agents at the code once the review started, the firm had Claude and Codex build the tooling first: a language server, a decompiler, a static analysis engine, and a translator that renders procedures into the Lean proof assistant. "Before code review even starts, agents now allow us to build custom tooling and formal models that improve the quality and depth of our reviews," Dahlgren writes.

The tooling found a high-severity vulnerability during the audit itself: an underconstrained advice value in a modular-reduction procedure that could let a malicious prover forge Falcon signatures and "drain any Miden account controlled by a Falcon key pair." Static analysis built on the decompiler's intermediate representation also flagged more than 400 locations across the library's public API where type validation could be improved. Separately, 95 agent-generated Lean proofs covering the core library's binary arithmetic caught two further bugs that the existing unit-test suite had missed entirely: an edge case in a 64-bit rotation, and a multiplication routine that dropped caller-owned values from the stack.

Dahlgren frames the shift in economic terms rather than capability terms: agents becoming reliable enough to carry speculative, non-essential work with only light supervision changed which projects are worth attempting at all. "Today, a failed side project only costs tokens," he writes. Six months of speculative tooling work is not something most audit engagements would have budgeted for even two years ago.

Why it matters: Most coverage of agents in security work is about agentic code review itself. This is a different claim: that the higher-value use of agent time may be building the verification infrastructure a review runs on, before the review starts. The payoff here was a real vulnerability plus two bugs no test caught, and the formal-proof result is a useful data point for anyone building a verification loop around agent output: unit tests missed two bugs that a machine-checked proof caught.