Trail of Bits’ Zero-Knowledge Audit Turns AI From a Bug Finder Into a Tool Builder

Trail of Bits, a security research and consulting firm, published an account this month of an audit that inverts the industry’s current AI narrative. Instead of pointing a coding agent at a finished codebase and cataloging the bugs it finds, the firm spent six months having agents build the review infrastructure itself: a language server, a decompiler, a static analyzer, and a formal proof assistant, for a zero-knowledge virtual machine that had none of that tooling to begin with. The investment paid off before a human reviewer read a single procedure: the tooling caught a bug that could have let an attacker forge cryptographic signatures and drain funds from any account secured by them.

The write-up, authored by Trail of Bits engineer Fredrik Dahlgren, is explicit about the contrast it draws with the rest of the industry. “Security firms have published numerous blog posts describing how they pointed their agent harness at a codebase and found dozens of bugs (we’re one of them),” Dahlgren writes. “However, these posts tend to focus on agentic code review, which is just one aspect of how we use AI in our security reviews. We want to give a different perspective: before code review even starts, agents now allow us to build custom tooling and formal models that improve the quality and depth of our reviews.”

A Blockchain With No Developer Tools At All

The subject of the audit was Miden VM, a STARK-based zero-knowledge virtual machine incubated by Polygon and built around a privacy-focused finance stack; the project’s own site describes its goal as “practical privacy for the future of finance,” and it is currently running a public testnet ahead of a mainnet launch. Trail of Bits was brought in during late 2025 to review the Miden core library, a set of cryptographic primitives written in Miden’s own custom assembly language, MASM.

MASM presented an unusual problem before a single bug was even in scope: almost no developer tooling existed for it. Miden VM is a stack machine, meaning every instruction reads its inputs from a shared stack and writes results back onto it, so inputs and outputs are always implicit rather than named. Most procedures in the core library have no declared signatures, MASM has no fixed calling convention, and net stack effects generally can’t be determined by reading the code alone, so an analysis failure at one point silently propagates through every call that depends on it. Loops don’t have to leave the stack in a consistent state between iterations, meaning a loop condition can occupy a different stack slot on each pass. There was no IDE support, no language server, and no linter. Dahlgren’s team had roughly six months before the implementation would be feature-complete enough to review, and used most of it building tools they didn’t yet have.

Six Months of Building Tools Before Reviewing a Line of Code

An LSP Server in Days

The first tool was a Language Server Protocol (LSP) server with a companion VS Code extension: the baseline navigation features (syntax highlighting, go-to-definition, finding references) that any modern codebase gets for free but that MASM had none of. Dahlgren says Claude produced a working prototype “within a few days,” after which the team layered in MASM-specific features: inline instruction documentation and per-instruction stack effects displayed directly in the editor, so a reviewer wouldn’t need to context-switch to look up what an opcode did to the stack.

A Decompiler Built by Committee

Stack-machine decompilation is a well-studied problem in the abstract, but MASM’s specifics (undeclared calling conventions, non-stack-neutral loops, branch-dependent stack effects) made faithfully decompiling the whole language impractical to guarantee. Trail of Bits scoped the tool to decompile a well-defined subset of MASM correctly, rather than attempt everything, and built it with agents alternating roles: Claude wrote and extended the decompiler, Codex reviewed the code, and after each new feature the team had agents decompile a randomized sample of real procedures from the core library and diff the output against the original MASM to catch regressions, which were then converted into permanent regression tests.

A Static Analysis Engine That Can’t Miss a Case

The static analyzer used abstract interpretation, a technique where the analysis doesn’t execute the program with real values but instead tracks what type of value could occupy each stack slot (“a 32-bit integer,” “unknown”) and repeats the pass until no new information emerges. Because it tracks every possible value at each step rather than sampling specific inputs, a check that passes under abstract interpretation is guaranteed to hold on every real execution of the program, not just the cases a reviewer happened to think to test. The team used it to answer three questions across the whole core library: are prover-supplied advice values, precomputed inputs like remainders and modular inverses that the prover supplies through a separate advice stack, properly validated before use? Are type constraints enforced? Are local variables initialized on every execution path?

A Formal Model in Lean

The most ambitious tool addressed a question code review can’t answer on its own: if a procedure looks correct, can you prove it’s correct for every possible input, not just the ones you tested? Dahlgren’s team built a minimal Miden VM executor inside Lean, which describes itself as “an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code,” and had Claude build an automatic translator from MASM procedures into Lean. During the review, multiple agents worked in parallel to prove correctness properties for as many core-library procedures as possible.

What Six Months of Preparation Found

The static analyzer’s abstract-interpretation passes, run during the actual review, flagged more than 400 distinct locations across the library’s public API where type validation could be tightened, plus one high-severity finding. That finding was in a procedure called mod_12289, which reduces a 64-bit value modulo 12289 using a quotient and remainder supplied by the prover as advice values. The quotient was checked to confirm it was a valid 64-bit integer. The remainder was not: it was passed straight into the 32-bit instruction u32overflowing_sub without ever being validated. By choosing a quotient and remainder that satisfied the subtraction’s own internal constraints while still being individually invalid, Trail of Bits found it was possible to make mod_12289 return an incorrect remainder. Because Miden’s Falcon signature verification depends on mod_12289, a malicious prover could use the bug to forge Falcon signatures and drain any Miden account secured by a Falcon key pair.

The Lean formal-verification effort caught two further bugs of its own, both edge cases the project’s existing unit test suite had missed entirely: a 64-bit right-rotation (rotr) that behaved incorrectly on inputs larger than Miden’s underlying Goldilocks prime field when the rotation shift was itself a multiple of 32, and a 256-bit multiplication (wrapping_mul) that silently dropped values the calling procedure still owned off the stack before returning. Even the correctness proofs needed a human check: reviewing the rotr proof surfaced that it required an extra, unstated assumption (that the shift wasn’t itself a multiple of 32) before the proof would actually go through, a gap a reviewer caught by reading the theorem statement, not by re-deriving the proof by hand.

Proving Absence Is a Different Job Than Finding Presence

That last detail points at what separates the Lean work from ordinary code review, agentic or otherwise. A reviewer, human or AI, that reads code and finds bugs is sampling; however careful the sampling, it can always miss a case nobody thought to check. A machine-checked proof makes a universal claim instead: it says a procedure behaves correctly for every input that satisfies its stated preconditions, not just the ones exercised by a test suite. Trail of Bits didn’t have to manually verify that each of the 95 Lean proofs it generated was internally sound, since Lean’s own trusted kernel does that automatically and can’t be talked into accepting a broken proof. What the team had to review instead was much smaller: whether each theorem’s statement actually captured the right correctness property for its procedure. Get the statement right, and a passing Lean proof is a stronger guarantee than any amount of code review, agentic or human, could offer on its own. The mod_12289 exploit condition, choosing a quotient and remainder that individually break validation while jointly satisfying the subtraction’s constraints, still had to be worked out by the review team; the Lean proofs still needed a human to check the theorem statements were the right ones.

Trail of Bits isn’t the only security team that landed on a similar combination this year. In July, Microsoft Research open-sourced machine-checked Lean proofs showing that new Rust implementations of SHA-3 and ML-KEM inside SymCrypt, its core cryptography library running in Windows, Azure Linux, and Xbox, match their published specifications. Microsoft’s approach used the same underlying pattern: source code translated automatically into Lean, using a Rust-to-Lean tool called Aeneas rather than a custom in-house translator, with the resulting proofs checked by Lean’s own trusted kernel rather than by hand. Two unrelated organizations landing on the same combination, an automatic translator into Lean paired with proofs checked by Lean’s kernel, within a few months of each other and on completely different codebases, is a stronger signal than either result alone that this is becoming a recognized security-engineering pattern rather than a one-off experiment.

Why This Wasn’t Worth Doing Two Years Ago

Dahlgren is candid about why Trail of Bits didn’t build this kind of tooling before now: the economics didn’t work. “The tools we developed leading up to this engagement… are all side projects that we wouldn’t have been able to dedicate time or resources to just one or two years ago,” he writes. “Projects like these are often highly exploratory in nature, and the end results and potential payoff may be difficult to predict. In practice, this means that it is hard to sell clients on them in advance. However, over the last year, agents became good enough to carry non-essential projects like these with only light supervision, which completely changed the economics of which projects are worth pursuing. Today, a failed side project only costs tokens.”

That’s a narrower and more falsifiable claim than the industry’s usual “AI makes security better” framing. It isn’t that agents review code better than humans: the exploit condition for mod_12289 still had to be worked out by a person once the analyzer flagged the location, and the Lean proofs still needed a person to sign off on what each theorem actually claimed. The claim is about capital allocation. Work that used to be too speculative to justify billing a client for, building an LSP server for a language nobody had tooled yet, on the chance it might later surface a bug, is now cheap enough in tokens that a security firm can simply do it and see what happens. The static analysis engine Trail of Bits built for this one engagement has already outlived it: the team says it has adopted the tool going forward, so it will help secure future updates to the Miden core library too, which means the “failed side project” framing describes the downside risk of this approach, not its typical outcome.