Trail of Bits' agent-built Lean model turned up a Falcon signature forgery in the Miden audit

According to a dev.to post summarizing Trail of Bits' own writeup ^[17], the hard part of MASM is that stack effects are not local. A while-loop need not be stack neutral, so its condition can sit in a different slot on each iteration, and each branch can carry its own stack effect ^[3]. The net stack effect of a call is generally impossible to determine statically. Each analysis failure propagates up the call chain ^[4]. The documentation is near zero, and the calling conventions are exactly zero ^[5][2].

The engineering I would defend at a review is how the team checked the tooling its agents wrote. Claude handled planning and development, and Codex reviewed the decompiler ^[9]. The decompiler covers a well-defined subset of MASM, chosen because it could be decompiled correctly. The alternative, per the post, was a full pipeline that would be silently wrong ^[8]. Every new feature went through the same loop:

1. An agent builds the feature ^[9]. 2. Agents decompile a randomized set of core library procedures ^[10]. 3. The output is diffed against the original MASM to find regressions ^[10]. 4. Anything found is added as a regression test ^[10].

The original MASM is the oracle in that loop ^[10]. The second model's review sits on top of it ^[9]. I think that ordering is right for agent-generated code, because the diff does not depend on either model's judgment.

The payoff landed away from the effort. The decompiler absorbed the most work ^[7], yet the post says its main value was its internal analysis frameworks and intermediate representation, reused for static analysis ^[13]. "If you pay an agent to build tooling, the intermediate artifacts are often the prize, not the surface output," the author wrote ^[14]. The forgery finding came from the Lean model of the VM executor. Its proof work produced 95 machine-checked correctness proofs over a large component of the core library ^[11][12].

The post extends the lesson to review of AI-generated code generally. "A bigger reader model just makes the wrong thing faster," the author wrote ^[15]. The author argues the bottleneck in PR review is the hours a change waits in queue and the size of the surface to trust, and was never the minutes spent reading a diff ^[16]. The Miden case supports a narrower claim. For the result to transfer to an ordinary pull-request queue, the constraint in that queue would also have to be missing tooling. In the post's telling, that was the constraint for MASM, a custom assembly language with no developer tooling ^[5].