Prove It, Don’t Read It: Contract-First Verification of AI-Generated Code with Sealed Contexts and Evidence-Graded Verdicts

Abstract

Large language models now write code faster than people can meaningfully read it, yet the dominant acceptance interface for AI-generated code is still line-by-line human review. We argue that this interface neither scales nor reliably catches plausible-but-wrong programs, and that the artifact a human signs off on should change: from the implementation to a short, machine-checkable contract. We present holdtrue, an open-source verification harness built on this principle. Two AI contexts that never share memory split the work: an author turns a plain-language intent into a formal contract, which the human reads and approves; behind an information-flow curtain, an implementer writes code from the contract alone, never seeing the intent, the private reference oracle, or the held-out tests. A layered harness—strict static typing, symbolic-execution proof, property-based testing, held-out differential testing, a negative-probe that rejects vacuous contracts, and mutation analysis—runs in an unprivileged sandbox and returns one of four evidence-graded verdicts: GUARANTEED, ENFORCED, UNGUARANTEED, or FAILED. We describe the protocol and its threat model, the verdict semantics, a worked example, and a reference implementation with six language backends, and we argue that graded, evidence-backed verdicts are the honest interface for delegated programming