Proof-Carrying Coding

In Proof-Carrying Code (POPL 1997, later awarded most influential paper of its year), George Necula solved an adversarial trust problem elegantly: a host must run a binary from an untrusted source. Instead of trusting the source or laboriously analyzing the binary, the source attaches a formal safety proof - and the host runs a small, fast proof checker. The deep insight is asymmetric effort: constructing the proof is expensive and falls on the producer; checking it is cheap and falls on the consumer. The host stays sovereign without doing the producer’s work.

AI coding recreates the trust setup almost exactly: a prolific, not-fully-trusted producer (the model) delivers work to a receiver (your team) that cannot afford to redo it. With 96% distrusting AI code and only 48% consistently verifying, most teams currently resolve the dilemma by trusting anyway. Proof-carrying coding resolves it the 1997 way - with one honest difference that must be stated, not hidden:

The bottom row is why the analogy is load-bearing rather than decorative: in both systems, the entire design exists because verification is radically cheaper than reproduction. Evidence that costs more to check than redoing the work would be worthless - which is also the quality bar for what belongs in the record.

1. Producers attach, always. Every AI run delivers its change plus its record - the written task, the validations that ran, their results, what was skipped. No record, no review request.
2. Receivers verify, not reconstruct. The review starts from the evidence: scope against boundaries, criteria against results. Judgment time goes to architecture and trade-offs, not archaeology.
3. Nothing merges on trust alone. “The agent said it passed” is a claim, not evidence - validation authored outside the generating session is what makes the record checkable.
4. The record persists. Stored with the code, the records accumulate into the audit trail nobody had to write retroactively. The artifact’s structure, with a labeled sample, is on the evidence reports page.

The formal end of the idea is being rebuilt for agents: 2026 research on proof-carrying agent actions has agent actions carry machine-checkable justifications that a gate verifies before execution - Necula’s architecture, re-aimed at runtime governance. The pragmatic end, described above, is deployable today. Its limits deserve the same clarity: evidence raises confidence, it does not prove correctness; a record can be complete and the architecture still wrong, which is why the human gate stays; and the quality of the whole scheme is bounded by the quality of the task - vague mandates produce unfalsifiable evidence.

Proof-carrying coding is Reality Graph’s operating principle stated as a concept: every run is verified against its written task, and the change travels with its evidence report - produced as a byproduct, checked in minutes, stored with the code, local-first. What that record resolves into, a single outcome per run and the rule that keeps a run blocked even when every test is green, is described under how the outcome is decided. The principle stands without any specific tool; the tool exists because the principle is tedious to uphold by hand at AI volume.