Eine Schraube weiter — Wo die Grenze der KI-Automation liegt, und wie man sie typisiert

Ich teile die Skepsis. Voll-Automation ist Hype. Rice ist unentscheidbar; METRs 50-%-Zeithorizont liegt Anfang 2025 bei rund 50–110 Minuten (Verdopplung etwa alle 7 Monate); und verifizierer-akzeptierte Spezifikationen sind oft inkorrekt oder unvollständig. „Coding is solved" ist eine Marketing-Phrase ohne Träger. Ich bin nicht hier, um das zu bestreiten — ich bin hier, um eine Schraube weiterzudrehen.

Die konstruktive Frage ist nicht „klappt Automation?", sondern: Wo genau liegt die Grenze — und lässt sie sich typisieren?

Die Grenze ist das Setzen der Invariante

Meine Antwort, so scharf wie ich sie halten kann — zweierlei, sauber getrennt:

(i) Strukturell. Die Grund-Invariante ist im System nicht selbst-fundierbar. Jede Begründung bräuchte eine weitere Invariante — ein Regress, der nur durch einen Anker außerhalb des Prüfvorgangs terminiert. Das ist ein Argument, kein Beweis.

(ii) Normativ. Dass der Mensch diesen Anker setzt, ist eine Wahl — keine Unmöglichkeitsaussage über Maschinen. Ausdrücklich nicht Penrose-Lucas: Rice trifft Mensch und Maschine symmetrisch. Wir wählen den Menschen, weil Intent extern zum Generator und verantwortungsbehaftet ist.

Heute heißt Akzeptanz: ein Mensch liest einen Diff und glaubt. Ich ersetze das durch: eine Maschine entscheidet Konvergenz gegen eine externalisierte, getypte Referenz.

Die Architektur: Generator ⊥ Prüf-Orakel

Entscheidend ist die Architektur — und zwar zweiachsig. Generator und Prüf-Orakel sind mechanisch getrennt: die generierende Engine kann per Werkzeug-Allowlist keinen Code schreiben (fälschungssicher); das Orakel (Sync.SetzeSpecAligned) bindet Aligned an einen im Testcode abgedeckten Test, dessen Greenness die CI-Suite erzwingt (rot blockt den Merge) — Test-PASS, nicht bloßer Prozess-Exit-0.

flowchart TB
  H["Mensch — setzt die Invariante"]:::h --> SPEC["getypte Spec
externalisierte Referenz"]:::s
  GEN["KI-Generator
Werkzeug-Allowlist:
kein Schreibrecht aufs Gate"]:::gen --> CODE["Code + Tests"]:::c
  SPEC --> GATE{"Gate
Marker abgedeckt + CI-Suite grün?"}:::g
  CODE --> GATE
  GATE -->|"Test-PASS"| OK["Spec-Knoten: Aligned"]:::ok
  GATE -->|"rot in der CI · nicht nur Exit-0"| NO["blockiert → revert"]:::r
  classDef h fill:#13243a,stroke:#4c9aff,color:#e6edf3;
  classDef s fill:#13243a,stroke:#4c9aff,color:#e6edf3;
  classDef gen fill:#161b22,stroke:#9aa7b4,color:#e6edf3;
  classDef c fill:#161b22,stroke:#9aa7b4,color:#e6edf3;
  classDef g fill:#1c1606,stroke:#d29922,color:#e6edf3;
  classDef ok fill:#0f1b14,stroke:#3fb950,color:#e6edf3;
  classDef r fill:#2a1416,stroke:#f85149,color:#e6edf3;

Der Unterschied zu Kiro oder GitHub Spec Kit: dort erzeugt dasselbe System Spec, Code und Test — die Referenz ist nicht unabhängig vom Prüfling. Hier ist sie es.

Ehrlich die zweite Achse: Generator und Spec-Autor sind nur getrennt, wenn die Spec aus separater Quelle kommt. Schreibt dieselbe Modell-Instanz Spec und Code, korreliert der Fehler — und genau dort steht der Mensch als Dekorrelator. Ein zweiter, unabhängiger Agent könnte dieselbe Rolle einnehmen; dass es der Mensch ist, ist eine Setzung, kein Unmöglichkeitsbeweis.

Zwei öffentliche Belege — CI-grün, reproduzierbar

🎮 runenruf 46/46

Ein Spiel — der Existenzbeweis: der Loop kann gegen ein Orakel terminieren, das Exit-0 nicht glaubt. Tragende FsCheck-Property spec-siegel-lager-nichtnegativ über jeden Seed und jede Befehlsfolge. Ehrlich: die freundlichste Domäne — die Spec ist die Welt.

📒 ledger-casestudy 6/6

Ein doppisches Hauptbuch — das Gegenstück: echtes IO, ein veränderliches Requirement, int64-Cent statt Float. Hier ist „trifft das Modell die Welt" nicht leer.

Der naive erste Entwurf zieht eine Gebühr beim Sender ab und schreibt sie nirgends gut — Wert verschwindet. Die Invariante spec-werterhaltung (Gesamtsumme aller Konten konstant) fängt das ab — ohne dass je ein Diff gelesen wurde:

stateDiagram-v2
  [*] --> Gruen1
  Gruen1: Korrektes Modell · 6/6 gruen
  Gruen1 --> Rot: naives Modell injiziert (Gebuehr verschwindet)
  Rot: ROT — Falsifiable, after 4 tests
  Rot --> Gruen2: Fix = Doppik (Gebuehr als Gegenbuchung)
  Gruen2: Wert bleibt neutral · 6/6 gruen
  Gruen2 --> [*]

./demo-gate-at-failure.sh führt genau das reproduzierbar vor: grün → naives Modell → Orakel rot → revert. Der naive Entwurf behauptet, Geld verschwinde nicht; die Invariante verwirft ihn.

Review ist Konvergenz gegen die Spec, nicht der gelesene Diff.

Und es komprimiert: eine 1-Zeilen-Invariante über den FsCheck-Generator deckt einen unbeschränkten Eingaberaum ab — gegenüber 41 LoC Ledger-Domain und 125 LoC Runenruf-Sim. Du reviewst eine Zeile, keinen 41-bis-125-Zeilen-Diff. „Spec ist nur Code im Trenchcoat" hält hier nicht: eine Beispieltabelle leistet, was die Invariante leistet, in diesen Fällen nachweislich nicht.

Die Grenzen, ungeschönt

Zwei kleine Fallstudien, ein Spiel und ein Hauptbuch. Kein Issue-Tracker, keine unbeschränkte Autonomie — die ist nicht da, und ich behaupte nicht, dass sie es ist. Der Property-Layer (FsCheck) ist real in beiden Repos. Lean ist für Werterhaltung und Nichtnegativität bewiesen — proofs/Werterhaltung.lean, sorry-frei (#print axioms nennt für beide nur propext, Quot.sound), CI-verifiziert. Für weitere Invarianten: Roadmap, nicht behauptet.

Damit ist für zwei Invarianten die Kette Typen → Property → Beweis geschlossen: dieselbe Erhaltung wird getypt, über Zufallsfolgen geprüft und für jede Folge bewiesen. Der Mensch bleibt am Modell-Gate — operational und normativ, nicht metaphysisch.

Den Kern habe nicht ich erfunden

Lahiri nennt ihn eine Grand Challenge („Intent Formalization", arXiv:2603.17150, 2026). Storey nennt das Fehlen externalisierter Begründung „Intent Debt" (arXiv:2603.22106, 2026). Die getypte Spec ist genau dieses externalisierte Rationale. Kambhampatis LLM-Modulo benennt den externen Verifizierer als Quelle der Garantie (arXiv:2402.01817).

Ich beanspruche keine Priorität — „erster" wäre eine unbeweisbare Negativ-Existenzaussage. Konditional: mir ist keine publizierte Implementierung mit genau dieser Kombination bekannt — getypte externalisierte Spec + architektonisch getrennter Generator/Orakel + property-/beweis-verifiziertes Gate, für einen Kern-Invarianten bis zum sorry-freien Lean-Beweis durchgezogen. Neuheit ist eine Literatur-Aussage, kein Beweis.

Die Skeptiker haben die Diagnose recht. Ich liefere die Schraube danach.

Selbst nachprüfen

# Fallstudie A: Spiel (Existenzbeweis) — erwartet: 46/46
git clone https://github.com/Koschnag/runenruf && cd runenruf
dotnet test tests/Runenruf.Tests

# Fallstudie B: Hauptbuch (schlägt zurück) — erwartet: 6/6
git clone https://github.com/Koschnag/ledger-casestudy && cd ledger-casestudy
dotnet test tests/Ledger.Tests
lean proofs/Werterhaltung.lean   # sorry-frei: axioms [propext, Quot.sound]
./demo-gate-at-failure.sh        # grün → Falsifiable (rot) → grün

→ Portal: alle Belege & das Paper Geführte Tour (14 Folien) Paper (PDF, 20 S.)

F#, Lean, „sorry-frei" & Co — kurz erklärt

Für alle ohne funktionalen/formalen Hintergrund, je mit Java-Analogie:

F# — funktionale .NET-Sprache (Runtime wie C#), immutable by default, Pattern Matching. ≈ Java mit record + sealed + Pattern-switch, durchgängig.
Discriminated Union — ein Wert ist genau einer von N Fällen; so ist der SPOT-Graph getypt. ≈ sealed interface + records + erschöpfendes switch.
Lean 4 — ein Theorembeweiser: der Compiler prüft einen mathematischen Beweis. Anders als Tests (Stichproben) gilt er für jeden Fall. ≈ am nächsten Dafny / JML+KeY.
„sorry-frei" — sorry ist Leans Platzhalter „Beweis ausgelassen" (eine Lücke, die trotzdem kompiliert). sorry-frei = keine Lücke; #print axioms zeigt nur Standard-Axiome, keine Schummel.
Property-based Testing (FsCheck) — prüft eine Eigenschaft über hunderte Zufallseingaben und „shrinkt" Fehler auf das minimale Gegenbeispiel. ≈ jqwik / QuickCheck.
Orakel — der Schritt, der „fertig/korrekt?" entscheidet; hier: grün nur bei echtem grünem Test, nicht bei „Agent sagt fertig".

Quellen

Lahiri, Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents, arXiv:2603.17150 (2026).
Storey, From Technical Debt to Cognitive and Intent Debt, arXiv:2603.22106 (2026).
Kambhampati u. a., LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks, arXiv:2402.01817 (2024).
METR, Measuring AI Ability to Complete Long Software Tasks, arXiv:2503.14499 (2025).
Misu, Ma, Lopes, VeriAct: Beyond Verifiability, arXiv:2604.00280 (2026).