Trail of Bits Miden Audit Found a Falcon Flaw After Agents Built the Missing Tools

Trail of Bits spent six months preparing for the Miden audit, then found a high-severity flaw with tools its AI agents had built from scratch. The Trail of Bits Miden audit involved more than pointing a model at source code. Its agents created an LSP server, decompiler, static analysis engine, and Lean model before the formal review began.

That preparation exposed an underconstrained value that reportedly could let a malicious prover forge Falcon signatures and drain affected accounts. The analyzers also identified more than 400 locations where type validation could improve. Meanwhile, the formal verification effort produced 95 machine-checked correctness proofs and uncovered two bugs missed by existing unit tests.

The important contest is not AI agents versus human auditors. It is direct AI code review versus agent-assisted construction of the infrastructure that makes difficult code review possible. Trail of Bits still relied on human supervision, manual theorem review, and conventional security judgment. The agents changed which supporting projects were economically practical.

The Trail of Bits Miden Audit Started Six Months Early

The decisive work began before auditors received a finished target to inspect.

The Miden team approached Trail of Bits in late 2025, according to the firm's detailed Miden audit account. Miden wanted parts of its zero-knowledge virtual machine reviewed before launch. One portion covered a core library containing cryptographic primitives written in Miden Assembly, or MASM.

A zero-knowledge virtual machine, often shortened to zkVM, proves that a program executed correctly without requiring every verifier to repeat that computation. Miden uses a stack-machine architecture. Instructions consume values from a stack and place their results back on it.

That architecture matters because inputs and outputs are often implicit in MASM code. A reviewer must track how each instruction changes the stack, then carry that state across branches, loops, and procedure calls. Familiar source-level cues can disappear.

MASM also lacked much of the tooling auditors normally expect. There was little editor support, no mature language server tailored to review, and limited automated analysis for the core library. Trail of Bits knew the implementation was not yet feature complete, but it also knew the review was six months away.

The firm used that window to build its own review environment. Claude produced an initial language server prototype within days, Trail of Bits says. The resulting MASM language server provides navigation, reference discovery, hover documentation, syntax diagnostics, instruction descriptions, and stack-effect information.

Those features sound like ordinary developer conveniences. In an unfamiliar assembly language, they become part of the security method. Navigation helps auditors trace a value across procedure boundaries. Inline stack effects reduce repeated manual reconstruction. Diagnostics expose assumptions before they become findings.

Trail of Bits then expanded the project into decompilation, static analysis, command-line tooling, and formal modeling. Claude handled planning and implementation tasks, while Codex participated in code review. The agents also switched roles, giving the generated work a separate review pass.

This was not a one-shot generation process. After implementing a feature, the team asked agents to decompile randomized procedures and compare the results against the original MASM. Regressions became tests, and the model then worked against those tests.

That feedback loop is central to the story. The agents were not treated as authorities whose output deserved automatic trust. They operated inside a growing verification system containing tests, review stages, analyzers, and later, a proof checker.

The audit therefore started with a different question from the usual one. Trail of Bits did not ask only whether an agent could find vulnerabilities. It asked which missing instruments prevented auditors, including agents, from understanding the code in the first place.

That change in scope created the conditions for the eventual findings. It also placed pressure on security teams that market AI review mainly as faster source-code scanning. The Trail of Bits approach required more preparation, but it converted that preparation into reusable technical infrastructure.

The Decompiler Became More Valuable Than Its Output

The decompiler mattered most because its internal representation gave other analyses a reliable place to operate.

Decompiling MASM was not simply a matter of replacing assembly instructions with readable expressions. Most core-library procedures lacked declared signatures, so the tools often had to infer their inputs and outputs from context. Procedures also lacked a uniform calling convention.

Loops created another problem. A MASM while-loop does not have to preserve the same stack shape between iterations. Its condition can move to another stack position, breaking simple attempts to assign stable names to instruction inputs.

Conditional branches can also produce different stack effects. If one branch adds an item while another removes one, the decompiler cannot blindly merge their states. Errors in stack-effect inference can then propagate through every procedure that calls the affected code.

Trail of Bits responded by limiting its promise. Its MASM decompiler targets a well-defined subset rather than claiming perfect recovery for every procedure. That choice placed correctness ahead of superficial coverage.

The decompiler became the largest tooling effort in the project. Trail of Bits reports more than 100 AI-generated commits across several months. Yet the finished pseudocode was not its most consequential output.

The project created an intermediate representation, or IR, that expressed procedure inputs and outputs as analyzable expressions. An IR is a structured version of code designed for transformation or analysis. Once MASM instructions existed in that form, the team could apply established data-flow and static-analysis techniques.

The analyzer could ask whether prover-supplied values were validated before use. It could track whether code enforced expected types, such as 32-bit integers or Boolean values. It could also determine whether local variables were initialized on every possible execution path.

Trail of Bits used abstract interpretation for part of this work. Abstract interpretation evaluates categories of possible values instead of executing a program with one concrete input. A value might be represented as a valid 32-bit integer, a Boolean, or an unknown value.

The analysis repeats until it reaches a stable state where no new information appears. When designed soundly, it overapproximates what real executions can do. That can produce false positives, but it should not silently exclude a real behavior covered by the model.

This illustrates why the Trail of Bits Miden audit differs from a generic AI coding demonstration. The agent-generated decompiler was not trusted to pronounce the code safe. It helped construct a substrate on which explicit, inspectable analyses could run.

The workflow also created benefits for humans. Decompiled procedures made high-level control and data flow easier to review inside the editor. Stack annotations reduced mental bookkeeping. Command-line interfaces made the same capabilities available to automated review processes.

There is a broader lesson for teams evaluating coding agents. The most valuable generated artifact may not be the one users see. A partially scoped decompiler can still justify its cost if its parser, control-flow model, and IR unlock several higher-value checks.

That conclusion also changes how teams should preserve project context. Agent prompts, regression cases, architectural decisions, and reviewer comments become durable engineering inputs. A searchable knowledge base can help keep those materials available across long security projects.

Direct AI review usually begins with the target code and asks for defects. Trail of Bits instead used agents to alter the review surface. The next result showed why that distinction mattered.

One Missing Check Reached Falcon Authentication

A single unvalidated remainder reportedly turned an arithmetic helper into a path for forged authentication.

During the audit, the static analyses identified more than 400 unique locations where type validation could be improved. Trail of Bits says all were reachable from the core library's public API. Many arose because procedures exposed publicly could be called without the assumptions their original authors expected.

A public procedure cannot safely rely on every caller to supply a value of the intended type. In a proof system, it is especially important to distinguish a value provided by the prover from a value constrained by the proof. Merely placing data into a computation does not establish that it represents the claimed integer or Boolean.

The high-severity finding centered on mod_12289, a procedure that reduces a 64-bit value modulo 12,289. The prover supplied a quotient and remainder through an advice mechanism. Advice values are execution hints computed outside the VM, often used to avoid expensive in-VM work.

The quotient received a check confirming it fit the expected 64-bit representation. The remainder did not receive equivalent validation before entering u32overflowing_sub, a 32-bit subtraction instruction.

Trail of Bits says an attacker could vary the quotient and remainder while still satisfying the subtraction constraints. That allowed mod_12289 to return something other than the mathematically correct remainder.

The bug's reach extended beyond an incorrect arithmetic result. The procedure supported Falcon signature verification. Falcon is a post-quantum digital signature scheme, and Miden used a variant in account authentication.

According to Trail of Bits, a malicious prover could exploit the underconstrained value to forge a Falcon signature and drain an account controlled by a Falcon key pair. That is the firm's technical claim, not an independently reproduced exploit presented in the public article.

The severity follows from Miden's execution model. The Miden VM design supports nondeterministic inputs supplied during proof generation. These inputs can improve efficiency, but the program must constrain them carefully.

A verifier does not infer the developer's intention. It checks whether the submitted proof satisfies the encoded constraints. If those constraints accept an invalid remainder, the proof can remain valid even when the claimed arithmetic relationship is false.

This is the core reversal. Zero-knowledge proofs can establish faithful execution of a specified system, but they cannot repair an incomplete specification. A cryptographic proof of an underconstrained program can provide confidence in the wrong property.

Independent context from a later Miden contract audit reinforces the general point. OpenZeppelin described Miden transactions as valid when a corresponding proof exists, making every MASM check part of the constraints a prover must satisfy.

That separate engagement covered a different repository scope and should not be conflated with Trail of Bits' review. However, both accounts show why authentication logic, prover-controlled inputs, and on-chain assumptions need explicit treatment.

The more than 400 type-validation locations should also be interpreted carefully. They were not described as 400 exploitable vulnerabilities. They represented places where validation could improve, with one reported high-severity issue among them.

That distinction matters because static analysis often finds conditions requiring triage. A sound analyzer may intentionally report more cases than eventually become security defects. Its value lies in systematically locating assumptions that deserve inspection.

For security teams, the result pressures a common shortcut: using an agent to summarize suspicious functions without first modeling the target language's value rules. A model can explain what code appears to do. The analyzer can ask whether every permitted execution actually respects the required type.

The Falcon finding came from combining both capabilities. Agents accelerated construction, while the static semantics turned an intuition about prover-controlled data into a repeatable check.

Lean Proofs Found What Unit Tests Missed

Formal verification did not replace testing, but it forced the team to state behavior precisely enough to expose two untested failures.

Trail of Bits pursued formal modeling even after building the editor and static-analysis tools. The question was deliberately different: if a library procedure contained no obvious defect, could the team prove that its implementation matched its intended arithmetic behavior?

The firm built a minimal Miden VM executor in Lean. Lean is an interactive theorem prover whose small trusted kernel checks whether a submitted proof follows from its definitions and assumptions. Claude also helped build a translator from MASM procedures into Lean representations.

Multiple agents then worked on procedure proofs in parallel. The resulting MASM Lean model contains executable VM semantics, translated procedures, shared proof support, and individual correctness theorems.

The repository lists 95 checked procedure proofs: 31 for 64-bit operations, 36 for 128-bit operations, 17 for 256-bit operations, and 11 for word operations. Together, they cover the binary-arithmetic portions described by Trail of Bits.

These were not proofs that every part of Miden was secure. They addressed defined correctness properties for particular procedures. That boundary is essential because a theorem prover verifies the theorem supplied to it, not the unstated intent in a developer's head.

Trail of Bits says human reviewers therefore focused on auditing theorem statements. If an agent proved a theorem that omitted a critical precondition or expressed the wrong result, kernel acceptance alone would not make the software correct.

At a high level, many theorems followed a recognizable pattern. Given a stack with specific inputs, executing a procedure should terminate and leave the mathematically expected result on top. Unrelated caller-owned stack values should remain in the expected locations.

That specification pressure exposed two defects missed by existing unit tests. The first affected a 64-bit right-rotation procedure named rotr. It behaved incorrectly for large inputs above the Goldilocks prime when the rotation amount was a multiple of 32.

The Goldilocks prime defines the field used by the VM, so values near or beyond that boundary require careful representation. During proof work, the desired theorem would not go through without adding an assumption that excluded the problematic shift case.

A failed proof is not automatically evidence of a code bug. The theorem, model, or supporting lemmas can also be wrong. Here, manual review of the obstruction led the team to the implementation edge case.

The second bug appeared in the 256-bit wrapping_mul procedure. Trail of Bits says it removed values owned by the caller from the stack before returning. Ordinary tests of the multiplication result could pass while failing to check preservation of surrounding stack state.

That defect shows why precise postconditions matter. A procedure can compute the correct numeric answer while violating its calling contract. In a stack machine, damaging adjacent state can affect later execution even when the top item looks correct.

Unit tests still play a central role. They execute quickly, protect against known regressions, and cover integration behavior that may not yet have a formal model. The Lean effort provided a different kind of assurance across explicitly stated properties.

The key advantage was compositional. Agents could produce proof attempts at scale, while Lean's kernel rejected invalid derivations. Humans did not need to trust the prose confidence of a model. They needed to examine the definitions and confirm that accepted theorems represented the intended guarantees.

This is a stronger control boundary than asking another language model whether generated code looks correct. It does not eliminate human judgment, but it moves that judgment toward specifications and assumptions.

For engineering leaders, the case suggests a practical division of labor. Agents can generate repetitive proof scaffolding, translators, and candidate lemmas. Human specialists decide what must be proven and investigate why important statements fail.

The Result Does Not Make Autonomous Audits Trustworthy

The project supports agent-assisted audit engineering, not unsupervised security certification.

Trail of Bits frames the economic change directly. A few years earlier, it would have struggled to justify months of exploratory tooling for one engagement. Such side projects had uncertain outcomes and were difficult to sell before their value became visible.

The firm argues that agents reduced the cost of exploration enough to change that calculation. Failed experiments increasingly cost tokens and supervision time rather than a full allocation of specialist engineering labor.

That claim deserves a careful reading. Six months still elapsed before the audit, and the decompiler alone accumulated more than 100 AI-generated commits. The public account does not provide a controlled comparison of staff hours, total model costs, or defect yield against a conventional engagement.

It also does not establish that agents can build equivalent tooling for every unusual language. MASM offered properties favorable to analysis and formal modeling. The Miden VM has a compact instruction set, and many operations avoid complex side effects.

Even within this favorable target, the decompiler could not safely cover every procedure. Trail of Bits narrowed its supported subset because inconsistent stack effects and missing signatures made complete, reliable decompilation impractical.

The Lean workflow carried another limit. Kernel-checked proofs establish only the stated theorem under the modeled semantics. A mistranslated instruction, incomplete VM model, or weak theorem can preserve a gap between proven behavior and real deployment.

Human review remained visible throughout the process. Auditors reviewed agent-generated code, converted regressions into tests, inspected theorem statements, and analyzed failed proofs. Claude and Codex alternated between development and review rather than operating as an unobserved authority.

This makes the primary comparison sharper. Direct AI review asks a model to recognize vulnerabilities in an existing representation. Tool-building agents help experts create a representation where missing constraints, invalid types, and incorrect postconditions become explicit.

Neither approach should stand alone. Models can surface hypotheses that static analyzers do not encode. Static analysis can cover execution paths that a probabilistic reviewer may overlook. Formal proof can then address selected properties with a machine-checkable standard.

The process also creates maintenance obligations. Parsers must follow language changes. Analyzers need regression suites. Formal models must remain aligned with VM semantics. Generated tooling that goes stale can create false assurance.

Trail of Bits reports that the Miden team adopted the static analysis engine for future core-library updates. That is an important signal because it moves the tooling beyond a single audit snapshot. Continued use will test whether the analyzer remains useful as the language and library evolve.

Organizations considering a similar workflow should also plan for provenance. Teams need to know which model generated a change, which human reviewed it, which tests ran, and which assumptions entered a proof. An engineering workflow is only as reviewable as the records preserved around it.

The public evidence therefore supports a bounded conclusion. Agents made an ambitious preparation program feasible for this engagement. The security assurance still came from the combined system of domain experts, tests, explicit analyses, and proof checking.

That system is more interesting than the claim that an AI found a bug. It offers a concrete model for using imperfect agents without treating their confidence as evidence.

Three Signals Will Test Whether This Audit Model Lasts

The next test is whether agent-built assurance tools remain correct, adopted, and productive after the headline findings.

The first signal is continued integration of the MASM analyzer into Miden's development process. Trail of Bits says the Miden team adopted the static analysis engine for future core-library changes. Routine use in continuous integration would strengthen the case that audit tooling can become preventive infrastructure.

The important measure is not how many warnings it emits. It is whether new public procedures receive the required validation before release, and whether analyzer updates track changes in MASM semantics. Persistent false positives or stale models would weaken the result.

The second signal is expansion and maintenance of the 95 Lean proofs. Additional verified procedures would show that the initial model supports ongoing work rather than a fixed demonstration. Changes to existing arithmetic code should also trigger proof updates or failures.

Watch the boundary between translated code and hand-reviewed specifications. Automation that expands proof counts without strengthening theorem coverage would not provide the same assurance. Clear documentation of assumptions will matter as much as the raw total.

The third signal is replication by other audit teams and language ecosystems. Miden presented an unusually suitable combination: a custom language, missing tools, explicit proof semantics, and months of preparation time.

A repeated pattern across different zkVMs or low-level languages would support Trail of Bits' broader economic claim. Failure to reproduce it on systems with concurrency, complex memory, or large dependency graphs would reveal its limits.

The Trail of Bits Miden audit has already produced more than a speculative workflow. It delivered an editor integration, decompiler, analyzer, VM model, checked proofs, and concrete security findings.

The durable question is whether teams can keep those artifacts aligned with the systems they protect. Developers evaluating agent-assisted security should examine the repositories, inspect the modeled assumptions, and ask where machine-checkable controls replace model confidence. That is the standard worth carrying into the next audit.