Auditing a verified, AI-generated compiler by formalizing its context

Verified code generation is a promising way to build trustworthy software. Humans settle on a specification, and an AI writes both the implementation and a machine-checked proof that the implementation meets it. Thus, all remaining risk lies in the specification, and the specification must be audited. That audit is easy when the specification is small and self-contained. However, most software is one module of a larger system, and a module's specification may be neither small nor self-contained: it depends on what the rest of the system guarantees. We report on our audit of such a module: the autoprecompile optimizer of powdr, a compiler for zero-knowledge virtual machines (zkVMs). It had been ported to Lean by AI and proven correct against a human-reviewed specification. That specification was stated over a single chip, yet its correctness rested on unverified assumptions about the rest of the zkVM. We first tried to audit those assumptions manually, through reading and discussion, and we failed. So, instead, we applied more formalization, in three ways. First, the auditors edited the specification, rather than arguing about it. Second, we wrote a , which formalizes the module's context and derives the specification from it. Third, we dynamically validated the assumptions that survived, on real inputs, using decidable static analyses. We describe each methodology and the defects that it exposed.