Trail of Bits Uses AI Agents to Build Custom Security Tooling and Formal Proofs for Miden zkVM Audit

Trail of Bits demonstrated how AI agents enabled the rapid creation of specialized security tooling for the Miden VM, a zero-knowledge virtual machine with a custom assembly language (MASM) and minimal existing developer infrastructure. Over a six-month preparation period, agents built an LSP server, a decompiler, a static analysis engine, and a Lean model of the VM executor from scratch. These tools were not just for convenience; they directly identified real security flaws, including a high-severity vulnerability in the mod_12289 procedure where an unvalidated prover-supplied input allowed malicious provers to forge Falcon signatures and steal funds.

AI-Driven Tooling Development

The team leveraged Claude and Codex to build tools that addressed the unique challenges of auditing stack-machine code:

• LSP Server: Built in days, it provided syntax highlighting, code navigation, and inline stack effect documentation to reduce context switching for human reviewers.
• Decompiler: A major effort involving over 100 AI-generated commits, it lifted MASM procedures into high-level pseudocode. While full decompilation was difficult due to implicit stack effects and lack of calling conventions, the internal intermediate representation proved valuable for static analysis.
• Static Analysis Engine: Using abstract interpretation, the agents built passes to check for unvalidated advice values, type constraint enforcement, and uninitialized variables. This identified over 400 unique locations where type validation could be improved.

Formal Verification with Lean

Beyond bug hunting, the team used agents to pursue formal verification. They implemented a minimal Miden VM executor in Lean and used Claude to build an automatic translator from MASM to Lean. Multiple agents worked in parallel to prove correctness properties for core library procedures.

• 95 Machine-Checked Proofs: These covered all binary arithmetic components of the core library.
• Bug Discovery: The formal modeling process revealed two subtle bugs missed by unit tests: an edge case in the 64-bit right-rotation (rotr) and an issue in the 256-bit multiplication (wrapping_mul) that dropped caller-owned values.

Economic and Workflow Implications

The report highlights a shift in the economics of security auditing. Previously, exploratory projects like building custom LSPs or formal models were hard to justify to clients due to high labor costs and uncertain payoffs. With AI agents, these "side projects" became feasible because they primarily cost tokens rather than extensive human engineering hours. The resulting tools improved both manual and agent-driven review coverage, and the Miden team has since adopted the static analysis engine for future development.