Trail of Bits Builds MASM Audit Tools with Agents, Publishes 95 Lean Correctness Proofs

On September 18, Trail of Bits published a case study on auditing the Miden zero-knowledge virtual machine. Before the formal review, the team spent six months using agents to help build a language server, a decompiler, static analysis tools, and an execution model in Lean. The release presents a workflow that subjects model-generated output to program analysis and checks by a proof kernel. [Original case study](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

Miden’s assembly language, MASM, passes operands through a stack, requiring readers to track data locations at every step. The public language server brings stack changes caused by instructions, decompiled output, and type diagnostics into the editor. It can also detect cases where finite field elements are treated as 32-bit integers without the necessary validation, giving humans and agents access to the same analysis cues. [Tool repository](https://github.com/trailofbits/masm-lsp)

According to the team’s report, static analysis identified more than 400 locations where type validation could be improved, along with one high-severity issue: modular arithmetic did not sufficiently validate a remainder supplied by the prover, potentially allowing Falcon signature verification to be bypassed. Those locations should not be equated with 400 exploitable vulnerabilities. The report also did not provide a complete list of patched versions sufficient to assess the risk to current deployments. [Audit findings](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

For formal verification, MASM procedures are translated into Lean definitions, and their correctness is proved using an executable semantic model of the virtual machine. The public repository lists 95 checked procedures covering 64-bit, 128-bit, and 256-bit integer operations, as well as word operations. It also specifies a Lean version and provides instructions for building individual modules, giving outside researchers a starting point for reproducing the verification. [Proofs and verification steps](https://github.com/trailofbits/masm-lean)

The scope of each proof still requires individual review. For example, the theorem for the 64-bit rotate-right procedure explicitly assumes that the remainder of the shift amount divided by 32 is nonzero. Passing the proof kernel’s checks supports only the properties established under the specified model and assumptions; it cannot be generalized into a comprehensive security guarantee for the entire virtual machine. The team also explains that humans must still review whether the theorems describe the behavior they actually intend to verify. [Theorem limitations](https://github.com/trailofbits/masm-lean), [Human review process](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

For engineering teams, the useful lesson is to turn agents’ exploratory work into tools that can be run repeatedly. Adoption should begin by pinning the versions of the code under analysis and the semantic model, then checking unsupported syntax, theorem assumptions, and regression tests. The key question to track over time is whether these proofs and diagnostics continue to hold as the code changes.