Glonce

Trail of Bits builds custom AI-made tooling to audit the Miden zkVM

securityThe Glonce editorsHacker News🔥55Glonce rating55Impact65Novelty70Relevance90Surprise50Players50Credibility80
Trail of Bits builds custom AI-made tooling to audit the Miden zkVM

In late 2025, the team behind the Miden zero-knowledge VM asked security firm Trail of Bits to review part of its codebase before launch, specifically the Miden core library, a set of cryptographic primitives written in a custom, stack-based assembly language called MASM that had almost no developer tooling. Knowing it had six months before the implementation was feature complete, Trail of Bits decided to spend that time having AI agents (Claude and Codex) build tooling from scratch rather than starting the review immediately. First came an LSP server and VS Code extension, built by Claude within a few days, adding syntax highlighting, goto-definition, reference finding, and hover documentation for MASM. Next, and the largest single effort, was a decompiler: over 100 AI-generated commits over several months, with Claude handling planning and development and Codex handling code review in an alternating loop, checked against the original MASM to catch regressions. Decompiling MASM fully proved impractical because most procedures lack declared signatures, calls don't follow a fixed calling convention, and while-loops and branches can leave the stack in different states, so the team scoped the decompiler to a well-defined, correctly-handled subset. The decompiler's internal intermediate representation turned out to be more valuable than the full decompilation pipeline: it let the team build a static analysis engine using abstract interpretation to check, across the codebase, whether prover-supplied advice values (like remainders and modular inverses) were properly validated, whether type constraints were enforced, and whether local variables were initialized on every execution path. Separately, because Miden's instruction set is small and mostly side-effect free, the team also had Claude build an automatic translator from MASM to a Lean formal model, then ran multiple agents in parallel during the review to prove correctness of as many procedures as possible, with humans auditing only the theorem statements since Lean's kernel already validates the proofs themselves. During the actual review, the static analysis tooling flagged over 400 unique locations reachable from the library's public API where type validation could be improved, plus one high-severity finding: in the mod_12289 procedure, which reduces a 64-bit value modulo 12289 using a prover-supplied quotient and remainder, the quotient was checked for validity but the remainder was never validated before being passed to a 32-bit subtraction instruction. By carefully choosing quotient and remainder values that still satisfied the subtraction's constraints, the team showed mod_12289 could be made to return an incorrect remainder, which a malicious prover could exploit to forge Falcon signatures and drain any Miden account controlled by a Falcon key pair. The Lean modeling work produced 95 machine-checked correctness proofs covering the core library's binary arithmetic components, and along the way caught two subtle bugs the existing unit test suite had missed: an edge case in the 64-bit right-rotation rotr that misbehaved on large inputs above the Goldilocks prime when the rotation shift was a multiple of 32, and an issue in the 256-bit multiplication wrapping_mul that dropped caller-owned values from the stack before returning. Trail of Bits argues this kind of six-month, speculative tool-building side project would not have been economically viable one or two years ago, since its payoff is hard to predict in advance and clients are hard to sell on it; with agents now capable of carrying such exploratory work under light supervision, a failed side project now only costs tokens. The Miden team has since adopted the static analysis engine for ongoing work on the core library.

Key facts

  • Trail of Bits spent six months building an LSP server, a decompiler, a static analysis engine, and a Lean formal model for MASM, Miden's custom assembly language, before its scheduled review of the Miden zkVM core library began.
  • The decompiler took over 100 AI-generated commits, with Claude used for planning and development and Codex for code review in an alternating loop; its intermediate representation, more than full decompilation, powered the static analyzer.
  • The static analysis tooling flagged over 400 unique locations where type validation could be improved and one high-severity finding, in the mod_12289 procedure.
  • The mod_12289 bug left the remainder of a prover-supplied modular reduction unvalidated, letting a malicious prover forge Falcon signatures and drain any Miden account controlled by a Falcon key pair.
  • The Lean formal-modeling effort produced 95 machine-checked correctness proofs and caught two bugs the existing unit test suite missed, in the rotr right-rotation and wrapping_mul multiplication routines.

Why it matters

The post is a case study in using AI agents not for code review itself but for the groundwork before review: building bespoke developer tooling and formal models for a codebase that had essentially none. Trail of Bits argues that six months of speculative, AI-driven tool building only became affordable once agents got good enough to carry exploratory side projects with light supervision, changing which preparatory work is worth attempting before a paid audit even starts.

Who it affects

It concerns the Miden team, whose zero-knowledge VM and its core cryptographic library (written in the custom MASM assembly language) were reviewed before launch, and by extension anyone who would hold or control a Miden account secured by a Falcon key pair, since the high-severity bug could have let a malicious prover forge signatures and drain such accounts.

How to use it

Trail of Bits describes an internal workflow rather than a released product: MASM tooling (LSP server, VS Code extension, decompiler, static analysis engine, CLI interfaces) and a Lean-based formal model of the Miden VM executor, built by alternating Claude for development and Codex for review. The Miden team has since adopted the static analysis engine to help secure future updates to its core library.

How solid is it

The account comes directly from Trail of Bits, the firm that did the review, describing its own process and findings in specific technical detail, including the exact mechanism of the mod_12289 bug and the two bugs caught by formal modeling; the source does not name individual authors or state whether the high-severity issue was fixed before launch.

Risks and caveats

The source does not say how long the review itself took (only that six months went into tooling beforehand), whether the mod_12289 fix shipped before Miden's launch, or whether Miden VM has launched at all; it also gives no dollar estimate for potential losses, saying only that the bug could have led to millions of dollars in lost funds.

“What could we spend our time and tokens on to make sure that the review would root out as many bugs as possible in the codebase?”

— Trail of Bits