Auditing in the age of (good enough) AI

Summary

Trail of Bits describes a six-month effort to prepare for a security review of the Miden VM, a new zero-knowledge VM with its own assembly language, MASM. Its agents built an LSP server, a decompiler, a static analysis engine, and a Lean model of the VM executor. The tooling found real issues, including an unvalidated prover-supplied input that could let a malicious prover forge Falcon signatures and steal funds, and the Lean work produced 95 machine-checked correctness proofs.