Proof-Carrying Coding: Änderungen mit Belegen

In Proof-Carrying Code (POPL 1997, später als einflussreichstes Paper seines Jahrgangs ausgezeichnet) löste George Necula ein adversariales Vertrauensproblem elegant: Ein Host muss ein Binary aus nicht vertrauter Quelle ausführen. Statt der Quelle zu vertrauen oder das Binary mühsam zu analysieren, hängt die Quelle einen formalen Sicherheitsbeweis an - und der Host lässt einen kleinen, schnellen Beweis-Checker laufen. Die tiefe Einsicht ist asymmetrischer Aufwand: Den Beweis zu konstruieren ist teuer und Sache des Produzenten; ihn zu prüfen ist billig und Sache des Konsumenten. Der Host bleibt souverän, ohne die Arbeit des Produzenten zu wiederholen.

KI-Coding stellt die Vertrauenslage fast exakt nach: Ein produktiver, nicht voll vertrauter Produzent (das Modell) liefert Arbeit an einen Empfänger (euer Team), der sie sich nicht leisten kann nachzubauen. Bei 96 % Misstrauen und nur 48 % konsequenter Prüfung lösen die meisten Teams das Dilemma derzeit, indem sie trotzdem vertrauen. Proof-Carrying Coding löst es auf die Art von 1997 - mit einem ehrlichen Unterschied, der ausgesprochen gehört statt versteckt:

Die unterste Zeile macht die Analogie tragend statt dekorativ: In beiden Systemen existiert das ganze Design, weil Verifikation radikal billiger ist als Reproduktion. Belege, deren Prüfung mehr kostet als die Arbeit zu wiederholen, wären wertlos - das ist zugleich die Qualitätslatte dafür, was in den Nachweis gehört.

1. Produzenten hängen an, immer. Jeder KI-Run liefert seine Änderung plus seinen Nachweis - den schriftlichen Auftrag, die gelaufenen Validierungen, ihre Ergebnisse, das Übersprungene. Kein Nachweis, keine Review-Anfrage.
2. Empfänger prüfen statt zu rekonstruieren. Das Review beginnt bei den Belegen: Umfang gegen Grenzen, Kriterien gegen Ergebnisse. Urteils-Zeit fließt in Architektur und Trade-offs, nicht in Archäologie.
3. Nichts mergt auf bloßes Vertrauen. „Der Agent sagt, es besteht“ ist eine Behauptung, kein Beleg - Validierung außerhalb der generierenden Session macht den Nachweis prüfbar.
4. Der Nachweis bleibt. Beim Code gespeichert akkumulieren die Nachweise zum Audit-Trail, den niemand nachträglich schreiben musste. Die Struktur des Artefakts samt gekennzeichnetem Beispiel steht auf der Prüfbericht-Seite.

Das formale Ende der Idee wird gerade für Agenten neu gebaut: Forschung von 2026 zu Proof-Carrying Agent Actions lässt Agenten-Aktionen maschinell prüfbare Begründungen tragen, die ein Gate vor der Ausführung verifiziert - Neculas Architektur, neu gerichtet auf Laufzeit-Governance. Das pragmatische Ende, oben beschrieben, ist heute einsetzbar. Seine Grenzen verdienen dieselbe Klarheit: Belege erhöhen Konfidenz, sie beweisen keine Korrektheit; ein Nachweis kann vollständig sein und die Architektur trotzdem falsch - deshalb bleibt das menschliche Gate; und die Qualität des ganzen Schemas ist durch die Qualität des Auftrags begrenzt - vage Mandate produzieren unfalsifizierbare Belege.

Proof-Carrying Coding ist Reality Graphs Arbeitsprinzip als Konzept ausgesprochen: Jeder Run wird gegen seinen schriftlichen Auftrag verifiziert, und die Änderung reist mit ihrem Prüfbericht - als Nebenprodukt erzeugt, in Minuten geprüft, beim Code gespeichert, local-first. Worauf dieser Nachweis hinausläuft, ein Ergebnis pro Run und die Regel, die einen Run auch bei grünen Tests blockiert lässt, steht unter wie das Ergebnis zustande kommt. Das Prinzip steht ohne jedes bestimmte Tool; das Tool existiert, weil das Prinzip bei KI-Volumen von Hand mühsam durchzuhalten ist.