Trail of Bits Used AI Agents to Audit Miden's Crypto Code

Security firm Trail of Bits had AI coding agents build an entire toolchain from scratch, a language server, a decompiler, a static analysis engine and a formal-verification model, to audit Miden VM, a zero-knowledge virtual machine with its own custom assembly language and, at the start of the engagement, almost no developer tooling of its own. The six-month effort found a bug that would have let a malicious prover forge Falcon digital signatures and drain any Miden account protected by one, Trail of Bits engineer Fredrik Dahlgren wrote on the firm's blog Sept. 18.

Miden VM is a zero-knowledge virtual machine, meaning it runs a program and produces a compact cryptographic proof that the program executed correctly, without revealing every step of the computation to whoever checks that proof. The party generating that proof is called the prover, and Miden's design lets a prover attach a Falcon signature, a post-quantum signature scheme, to authorize spending from an account. If a prover can forge one, it can spend funds it does not control.

Dahlgren said the team, working with Claude and OpenAI's Codex, spent roughly six months building tooling for Miden Assembly (MASM), the custom stack-based instruction set the VM runs, before the manual code review even started. MASM had almost no existing developer tooling of its own when the engagement began, Dahlgren wrote, which is why the audit's first move was to have agents build the tools a reviewer would normally expect to find already in place. The reasoning, in Dahlgren's words: "a failed side project only costs tokens" once an agent is doing the typing, which changes which exploratory tools are worth building at all. The blog post does not name the specific model versions used, or how much of the six months went to directing the agents rather than letting them run unsupervised.

What the tooling built, and what it found

Tool	What it does	Result
LSP server and VS Code extension	Syntax highlighting, goto-definition, inline stack effects	Baseline tooling MASM lacked
MASM decompiler	Converts stack-machine code to readable pseudocode	Over 100 AI-generated commits
Static analysis engine	Built on the decompiler's intermediate representation	400-plus locations flagged for weak type validation
Lean formal model	Auto-translates MASM procedures into correctness proofs	95 machine-checked proofs

The critical finding came out of the core cryptography library: a procedure called mod_12289, which reduces a 64-bit value modulo 12289 using a quotient and remainder the prover supplies as untrusted input. Dahlgren's post says the code validated the quotient but never validated the remainder before passing it to a 32-bit subtraction instruction, letting an attacker choose a quotient and remainder pair that made the procedure return an incorrect result. That incorrect remainder was enough, the post says, to forge Falcon signatures and "drain any Miden account controlled by a Falcon key pair."

A fix that shipped before the post that explains it

Miden's own changelog credits version 0.23.0, released May 9, 2026, with having "fixed Falcon mod_12289 remainder validation and u64::rotr overflow handling for rotations by 0 and 32," filed under pull request #2968. Trail of Bits' post, describing the same bug in detail, did not go up until Sept. 18, more than four months later: the fix was already live and unremarked-on in a routine release before the public explanation of why it mattered existed.

The Lean proofs caught two further bugs conventional tests had missed, both bundled into the same fix: an edge case in 64-bit right-rotation (rotr) with large inputs, and a stack-handling issue in 256-bit multiplication (wrapping_mul). Neither is described as independently exploitable in the post; both are presented as correctness gaps formal verification surfaced that testing alone did not.

What the post does not claim

Dahlgren's write-up frames the 95 proofs as covering "a large component" of the Miden core library, not the whole of it, and does not say what fraction of the codebase the static analyzer's 400-plus flagged locations represent or how many turned out to be real bugs versus false positives. It also does not say whether the mod_12289 bug would have surfaced from a conventional manual review on the same timeline, without any of the agent-built tooling, which leaves open whether the tooling changed the outcome or only the economics of getting there. Those are the gaps a reader has to weigh before treating token-cheap agent tooling as a substitute for scoping an audit properly, rather than a way to audit more of the same scope for less money.

It is not the only forged-signature story on this beat this month: a UC San Diego-led team forged RSA-1024 signatures via a raw signing oracle rather than factoring the key, at a cost of 1,380 CPU core-years. Both cases turn on the same idea, that a signature scheme can fail through an implementation or protocol detail years before anyone breaks its underlying math, and both required an attacker with a specific kind of access, a raw signing oracle in one case and prover-controlled advice values in the other, rather than a break in Falcon or RSA themselves. Trail of Bits' agent-written tooling also arrives in a season of scrutiny over what AI-assisted development tools actually verify: CLI-Anything's own claims about its test coverage turned out to contradict each other, a reminder that a tool built by an agent still needs its output checked by something other than the agent that built it.