Agent-built tools uncover signature forgery bug in Miden zkVM

Security firm Trail of Bits said on 18 September 2026 that AI agents it used to build custom analysis tooling helped uncover a security issue in the Miden VM, a new zero-knowledge virtual machine, including an unvalidated prover-supplied input that the firm said would let a malicious prover forge Falcon signatures and steal funds from Miden account holders.

According to the blog post, the Miden team approached Trail of Bits in late 2025 to review parts of its zero-knowledge VM before launch. Part of the review covered the Miden core library, which contains a small set of cryptographic primitives written in a custom assembly language called Miden assembly, or MASM.

The firm said the project presented unusual difficulties. The Miden VM uses a stack-machine architecture, meaning each instruction reads values from the stack and writes results back to the top of it. Trail of Bits said that makes MASM code hard to review because instruction inputs and outputs are always implicit. Because the architecture is new, the company added, there was very little existing developer tooling such as IDE support, Language Server Protocol servers or linters.

With six months before the implementation was feature complete, the firm said it directed its agents at building the missing tooling rather than starting with code review. It reports that its agents produced an LSP server, a decompiler, a static analysis engine, and a model of the VM executor written in the Lean proof assistant, all from scratch.

For the editor tooling, the company said Claude built a working prototype within a few days that provided syntax highlighting, go-to definition, finding code references and docstrings on hover. The firm later added MASM-specific features, including inline instruction documentation and per-instruction stack effects, which it said avoids the context switch of looking up instruction semantics elsewhere.

The decompiler was the largest piece of work, with more than 100 AI-generated commits, according to the post. Trail of Bits describes several reasons that decompiling hand-written MASM is harder than it looks. Most core library procedures do not declare signatures, so the number of inputs and outputs has to be inferred from context. Procedures do not follow a well-defined calling convention, and the net stack effect of a call is generally impossible to determine statically, so analysis failures propagate up the call chain. While-loops need not be stack neutral, so a loop condition may sit in a different stack slot on each iteration, and different branches of a conditional may have different stack effects.

Because of those limits, the firm said it chose to decompile only a well-defined subset of MASM correctly rather than attempt full coverage. During development it alternated between using Claude for planning and implementation and Codex for code review. After each new feature, agents decompiled a randomised set of procedures from the core library and compared the output against the original MASM to check for regressions, with any issues added as regression tests for the model to fix.

The Lean work produced 95 machine-checked correctness proofs covering a large component of the Miden core library, the company said. Trail of Bits framed the exercise as a contrast to the common pattern of blog posts about pointing an agent harness at a codebase and reporting dozens of bugs, arguing that agents are also useful for building tooling and formal models before code review begins.