Auditing in the age of (good enough) AI
Trail of Bits published an account of how it used AI agents in a security review of the Miden VM, a zero-knowledge VM with its own custom assembly language, Miden assembly (MASM), and almost no developer tooling. The Miden team approached Trail of Bits in late 2025 to have parts of the VM reviewed before launch, with part of the scope covering the Miden core library, which holds a small set of cryptographic primitives written in MASM. Because MASM is a stack-machine architecture where instruction inputs and outputs are implicit, and because IDE support, LSP servers, and linters barely existed, Trail of Bits spent six months having its agents build an LSP server, a decompiler, a static analysis engine, and a Lean model of the VM executor from scratch. It says a Claude-built prototype LSP server and VS Code extension arrived within a few days, providing syntax highlighting, goto definition, code references, and procedure docstrings on hover. The post states that these tools found real security issues, including an unvalidated prover-supplied input that would let a malicious prover forge Falcon signatures and steal funds from Miden account holders. It also says the Lean work produced 95 machine-checked correctness proofs covering a large component of the Miden core library. Trail of Bits frames this as a different perspective on AI in security reviews: rather than focusing only on agentic code review, it describes agents building custom tooling and formal models before code review begins.
It illustrates agents being used to build language tooling and formal models that surfaced a signature-forgery flaw in a new zkVM before launch.