Security firm Trail of Bits published an audit report on the Miden zero-knowledge virtual machine: over six months of preparation, Claude and Codex agents built four tools from scratch — an LSP server, a decompiler, a static analyzer, and a formal model of the executor in Lean. These tools found more than 400 instances in the public API where values were not type-validated, and a critical vulnerability that allowed a malicious prover to forge Falcon signatures and drain any Miden account with a Falcon key. Formal verification produced 95 machine-checked proofs of correctness, and all four tools are open on GitHub.

image
image

What happened

On September 18, 2026, Trail of Bits published an audit report on the Miden zkVM, detailing the agent-based preparation phase of the review. Over six months, Claude and Codex agents built four tools from scratch for the Miden Assembly language: the masm-lsp LSP server, the masm-decompiler decompiler created by more than a hundred AI commits, the masm-analysis static analysis engine based on abstract interpretation, and the masm-lean formal model of the virtual machine executor in Lean. Together, these tools found more than 400 instances in the public API where values were not type-validated, and a critical vulnerability in the mod_12289 procedure: an unvalidated remainder value, supplied by the prover through the advice stack, allowed an attacker acting as a prover to forge Falcon signatures and drain any Miden account with a Falcon key. Formal verification produced 95 machine-checked proofs of correctness, covering all binary arithmetic in the core library, and identified two bugs missed by unit tests: an incorrect rotr on inputs larger than the Goldilocks prime when the shift is a multiple of 32, and a loss of stack values in wrapping_mul during 256-bit multiplication.

Context

MASM is a language without an ecosystem: it had no IDE, no LSP, no linters — meaning the basic infrastructure that any code audit relies on. Historically, the cost of building such a toolset for a single specific language made full audit preparation prohibitively expensive, so it was usually not done for exotic runtimes. The second element of context is the zk-specific trust boundary: in zero-knowledge systems, the prover supplies part of the input data through the advice stack, and a value accepted at this boundary without checking becomes an attack channel, not just a code inaccuracy. The third element is methodology: Claude was used for planning and development, Codex for code review, and findings were automatically degraded into regression tests, so the result is grounded in deterministic artifacts — a static analyzer, a formal model of the executor, and tests. Notably, formal proofs and unit tests caught non-overlapping classes of defects: verification complements tests rather than duplicating them.

Why this matters for the industry

For the industry, this is a shift in the economics of security auditing. Custom tooling for an exotic language, which was previously prohibitively expensive, can now be assembled in months by a small team: agent side-projects like a decompiler or a Lean model cost the price of tokens plus expert time for task setup and review. This undermines the price moat of large audit firms and opens a niche for vertical AI-security products; the first commercial offers in the form of "AI-augmented audit" are expected, along with pressure on pricing for audits of exotic languages. A second consequence is the shift from one-off audits to continuous verification: Miden has already implemented the static analyzer to check future updates to the core library, turning it into a deterministic gate in CI. If the trend holds, proof coverage of core-library-level arithmetic may become a hygiene minimum for cryptographic virtual machines, and competition among audit firms will shift to the quality of agent pipelines and expertise on top of them.

Why this matters for users

For the reader, this is a practical recipe, not a story about someone else's success. All four tools are open on GitHub: masm-lsp, masm-decompiler, masm-analysis, and masm-lean can be studied, applied to your own zk- or WASM projects, and the pattern can be replicated for your own language without an ecosystem. The Claude and Codex agents themselves are available to any developer, so the combination where one agent handles planning and development and the other does code review is reproducible without access to closed technologies. The case confirms that such a combination finds defects at the level of fund loss, not just code style notes.

What is still unknown / limitations

The "it only costs tokens" formula requires a caveat: six months of preparation is the time of Trail of Bits experts who set tasks for the agents, directed them, and reviewed the results, and it does not follow from the report that the Claude and Codex combination is reproducible without comparable expert load. Methodological metrics are not disclosed: the publication does not include the cost in tokens and money, the share of human oversight, the frequency of agent failures, or the false positive rate of the static analyzer. Finally, this is not a finished product, but a set of open components: transferring the methodology to another language will require its own engineering work and expert time to verify findings.

Sources

Author

Look at AI, editorial team