Building Compilers to Catch Exploits: How Trail of Bits Used AI Agents to Audit Miden zkVM

The mainstream narrative surrounding AI coding agents is dominated by a superficial premise: "Developers will copy and paste code into an LLM, and the model will point out the bugs."

In production cybersecurity, this approach is essentially useless. When reviewing mission-critical zero-knowledge rollups, financial infrastructure, or distributed systems, pasting raw assembly code into a chatbot yields hallucinations, shallow linter warnings, and a catastrophic false sense of security.

Recently, Trail of Bits—widely regarded as one of the world’s most elite software security research firms—published an extraordinary post-mortem: "Auditing in the Age of (Good Enough) AI."

Faced with the daunting task of auditing the Miden VM (a brand-new zero-knowledge virtual machine executing an esoteric, low-level stack-machine assembly language called MASM with zero developer tooling), Trail of Bits took an entirely different path.

They did not use Claude or Codex to read the code. Instead, they used AI agents to build an entire compiler and formal verification toolchain from scratch in six months.

The result? Their agent-built toolchain uncovered a severe cryptographic vulnerability in Falcon signature verification that would have enabled malicious provers to forge signatures and drain user funds on mainnet, alongside producing 95 machine-checked mathematical correctness proofs in Lean.

Here is an architectural breakdown of what Trail of Bits built, why "meta-tooling" represents the true frontier of coding agents, and the lessons systems architects must adopt today.

1. The Real-World Engineering Challenge: The Miden zkVM

To understand why traditional auditing failed, consider the mechanics of the target system:

Stack-Machine Architecture: Unlike register-based architectures (x86 or ARM), MASM operates on a 16-element stack. Instructions implicitly consume operands from the top of the stack and push results back.
Zero Static Type Information: Procedures lacked formal signatures; input parameters and return values had to be inferred entirely from execution context.
Dynamic Stack Depth: Loops and conditional branches frequently altered stack heights dynamically, making static analysis nearly impossible with standard linters.
Zero Existing Tooling: Because MASM was proprietary and new, there were no Language Server Protocol (LSP) servers, no IDE syntax highlighters, no decompilers, and no linters.

Human auditors looking at raw MASM were navigating completely blind.

2. The Agent Strategy: Building Meta-Tools, Not Chatting

Trail of Bits asked a fundamental question:

"What could we spend our time and token budget on to make sure the review would root out as many critical bugs as possible?"

Instead of treating agents as reviewers, they treated agents as compiler engineers across four distinct phases:

┌────────────────────────────────────────────────────────┐
│             AI Agent Orchestration Fleet               │
│  (Claude for architecture/planning, Codex for review)  │
└───────────────────────────┬────────────────────────────┘
                            │
        ┌───────────────────┼───────────────────┐
        ▼                   ▼                   ▼
┌───────────────┐   ┌───────────────┐   ┌───────────────┐
│ Custom MASM   │   │ Stack Machine │   │ Formal Lean   │
│  LSP Server   │   │  Decompiler   │   │ Correctness   │
│ & VS Code Ext │   │ (AST Lifting) │   │ Model & Proofs│
└───────┬───────┘   └───────┬───────┘   └───────┬───────┘
        │                   │                   │
        └───────────────────┼───────────────────┘
                            ▼
      ┌───────────────────────────────────────────┐
      │       High-Assurance Security Audit       │
      │ • Caught Falcon signature forgery exploit │
      │ • 95 machine-checked mathematical proofs  │
      └───────────────────────────────────────────┘

Phase 1: Rapid LSP Server & IDE Integration

In a matter of days, agents bootstrapped a full Language Server Protocol (LSP) server in TypeScript/Rust for MASM:

Real-time syntax highlighting and jump-to-definition.
Hover documentation for custom assembly opcodes.
Inline Stack-Effect Annotations: Rendering the exact expected stack state before and after every single instruction, eliminating cognitive context switching for human reviewers.

Phase 2: Building a Stack-Machine Decompiler

Reading stack-machine assembly is exhausting. Trail of Bits directed agents to write a decompiler that "lifted" MASM bytecodes into high-level control-flow graphs (CFGs) and structured pseudo-code.

Because hand-written assembly allowed non-stack-neutral loops, the agents scoped the decompiler to a provably sound subset of the language.
Reviewers could now view the high-level semantic intent in VS Code right next to the raw assembly.

Phase 3: Formal Verification in Lean (95 Machine Proofs)

Human review, even with decompilers, cannot guarantee that complex polynomial math is free of edge-case overflows.

Trail of Bits used agents to construct a formal mathematical model of the Miden VM executor in Lean 4.
The agents synthesized 95 machine-checked proofs of correctness, mathematically verifying that core cryptographic arithmetic primitives behaved identically to their formal specification under all possible inputs.

3. The Big Yield: Catching the Falcon Forgery Exploit

The ultimate test of any engineering methodology is real-world exploit prevention.

During this process, the agent-generated tooling flagged an unvalidated prover-supplied input within the Falcon signature verification routine. In zero-knowledge rollups, the prover generates cryptographic proofs that the verifier checks on-chain. If an input from an untrusted prover is consumed without mathematical constraints, the prover can synthesize fraudulent witnesses.

Had this reached mainnet:

A malicious actor could have forged signatures on behalf of arbitrary account holders.
Account funds could have been drained without possessing the private key.

A generic LLM prompt would never have found this bug. It was discovered only because agents had built a custom semantic analyzer that systematically verified input constraints across stack boundaries.

4. The Core Lesson for Software Architects

Trail of Bits has provided the industry with a masterclass in how to deploy coding agents effectively:

Stop asking agents to "find bugs": Ask them to build the specialized linters, fuzzers, parsers, and decompilers that make finding bugs trivial.
The leverage is in tooling velocity: Building an LSP server, VS Code extension, and decompiler used to take an engineering team six months. Agents collapsed that development timeline into days, leaving months of runway for actual verification.
Formal verification is no longer a luxury: With models like Claude and Codex capable of writing Lean proofs and property-based test suites, machine-checked mathematical correctness is entering mainstream systems engineering.

The future of software security belongs not to those who use AI as a search engine, but to those who orchestrate agents as compiler architects.

Sources & References: Trail of Bits Research ("Auditing in the age of good enough AI" by Fredrik Dahlgren), Miden zkVM Architecture Documentation, and Formal Methods in Lean 4.