Certificate-Carrying Patch Promotion: Verifier-First Gates for AI-Generated Repository Changes

Code-generating agents are increasingly evaluated by whether a patch builds or passes a test suite, yet repository changes often carry obligations that ordinary tests do not express: dependency constraints, artifact provenance, reproducibility, specification scope, and stronger semantic invariants. We formulate certificate-carrying patch promotion, a verifier-first contract in which trusted repository policy derives the obligations affected by a candidate and independently checkable evidence is required for each one. The generator may propose code and evidence, but it cannot lower the policy-required obligation set. We prove policy-relative compositional soundness, no-declaration-downgrade and no-free-scope-lift properties, and show that deriving obligations from an authenticated cumulative diff against a fixed trusted anchor makes the required set path-independent within a promotion transaction, preventing split-edit evasion. We instantiate the contract with a 16-case executable regression suite. A build-and-test baseline accepts all 16 cases, including eight deliberately unsafe patches; the typed gate accepts all eight safe cases and rejects all eight unsafe cases, with the result reproduced by a separate implementation. An exact two-file counterexample demonstrates why step-local obligation discovery can miss a non-decomposable policy. Existing policy-as-code, supply-chain attestation, and formal-verification systems provide important components; our contribution is the typed scope/trust-boundary contract for composing them around untrusted AI-generated patches.