Präsentation · zum Durchklicken · mit Live-Demo

Das Terminierungs-Orakel

Diszipliniertes KI-Coding: ein Loop mit einem fälschungssicheren Gate.

Cong Chanh Vinzenz Nguyen · F#/.NET · alles Open Source & CI-grün

weiter mit → · Übersicht Esc

Kein Vorwissen nötig.

Wir erklären alles über das, was du schon kennst:
CI · Code-Review · Tests · Typen.

Ziel: du verstehst, was gebaut wurde und warum — und probierst es selbst aus.

Der Trend: man baut Schleifen, nicht Prompts

Boris Cherny (Anthropic, Claude Code): „my job is to write loops." Die KI bessert sich selbst nach — bis ein Ziel erreicht ist.

flowchart LR G["KI-Generator"]:::g -->|"Vorschlag"| C{"Prüfschritt"}:::c C -->|"verworfen"| G C -->|"akzeptiert"| T{"fertig?"}:::t T -->|"nein"| G T -->|"ja"| D(["Terminierung"]):::d classDef g fill:#161b22,stroke:#4c9aff,color:#e6edf3; classDef c fill:#161b22,stroke:#9aa7b4,color:#e6edf3; classDef t fill:#1c2430,stroke:#d29922,color:#e6edf3; classDef d fill:#13241a,stroke:#3fb950,color:#e6edf3;

Die Architektur ist korrekt. Die offene Frage: woran hängt „fertig?"

Der blinde Fleck

Wenn „fertig" heißt: „der Agent sagt es" oder „die Tests, die er sich selbst schrieb, sind grün" —

— dann ist das ein selbst-genehmigter Pull Request.

  • Brute Force statt verbürgtem Endzustand
  • Blackbox — keiner versteht mehr das „Warum" (Cognitive Debt)
  • unkontrollierte Token-Kosten

Die Idee in einem Satz

Gib der Schleife ein Gate, so streng & unabhängig wie eine gute CI —

und erst wenn es grün ist, gilt „fertig".

Der Kern: Generator ⊥ Orakel

flowchart TB H["Mensch — setzt die Invariante"]:::h --> SPEC["getypte Spec"]:::s GEN["KI-Generator
darf KEINEN Code aufs Gate schreiben"]:::gen --> CODE["Code + Tests"]:::c SPEC --> GATE{"Orakel: echter Test grün?"}:::g CODE --> GATE GATE -->|"grün"| OK["Aligned ✓"]:::ok GATE -->|"rot / 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;

Wer Code schreibt, vergibt nicht selbst „grün". Sonst benotet sich der Agent selbst.

Die Referenz: der SPOT-Graph

flowchart TD SPOT["SPOT · Single Point of Truth
ein getypter F#-Graph, 1 JSON pro Knoten"]:::core SPOT --> A["Spec
(Given/When/Then)"]:::n SPOT --> B["Test"]:::n SPOT --> C["Risk"]:::n SPOT --> D["Invariant"]:::n SPOT --> E["Component · ADR · Begriff"]:::n classDef core fill:#13243a,stroke:#4c9aff,color:#e6edf3; classDef n fill:#161b22,stroke:#3fb950,color:#e6edf3;

Die Spec ist zugleich externalisiertes, geteiltes Wissen — gegen die Blackbox.

Der Fluss: Spec → Test → Code

cdd derive-tests   # je Akzeptanzkriterium ein Test-Knoten (KI-frei)
cdd derive-code    # xUnit-Skelett mit Marker + failwith TODO  (= ROT)
# Generator: Implementierung + echte Tests …
cdd sync-tests     # misst Konvergenz gegen das Gate

Tests sind Derivat der Spezifikation — nicht aus dem Bauch handgeschrieben.

Das harte Gate (Cdd.Core.Gate)

Früher: Aligned bei bloßer Marker-Präsenz — ein failwith-Skelett trägt den Marker, läuft aber rot.

flowchart LR T["Test-Knoten + Marker"]:::n --> Q{"echter Lauf grün?
passed>0 ∧ failed=0"}:::g Q -->|"ja"| AL["Aligned ✓"]:::ok Q -->|"nein"| PE["Pending — kein Fake-Grün"]:::r classDef n 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;

Maschinell bewiesen (FsCheck): ein nicht-grüner Lauf macht einen Knoten nie Aligned.

Jetzt selbst ausprobieren 👇

Wähle, was der Agent schreibt — und sieh das Gate live entscheiden. (Vollbild: demo.html)

Drei Verifikationsschichten

flowchart LR TY["Typen
illegale Zustände unrepräsentierbar"]:::a --> PR["FsCheck-Property
über unbeschränkte Eingaben"]:::b PR --> LE["Lean-4-Beweis
für JEDEN Fall, sorry-frei"]:::c classDef a fill:#161b22,stroke:#4c9aff,color:#e6edf3; classDef b fill:#161b22,stroke:#3fb950,color:#e6edf3; classDef c fill:#13243a,stroke:#d29922,color:#e6edf3;

Abgestuft nach Wichtigkeit. Zwei Invarianten sind bis zum Lean-Beweis durchgezogen (Werterhaltung, Nichtnegativität).

Ralph × CDD: der Loop bekommt sein Orakel

flowchart LR R["Ralph
Motor (Brute Force)"]:::r -->|"Tick"| GEN["Generator-Tick"]:::g GEN --> GATE["CDD-Gate
Validate → dotnet test → Marker"]:::o GATE -->|"rot"| GEN GATE -->|"alle Knoten grün"| DONE["Konvergenz (gemessen)"]:::d classDef r fill:#2a1416,stroke:#f85149,color:#e6edf3; classDef g fill:#161b22,stroke:#9aa7b4,color:#e6edf3; classDef o fill:#1c1606,stroke:#d29922,color:#e6edf3; classDef d fill:#0f1b14,stroke:#3fb950,color:#e6edf3;

Ralph ist der Motor, CDD ist Bremse + Lenkung. Failure-Diagnose fließt in den nächsten Tick → gerichtet statt blind.

Ehrlich: die Grenzen

  • Ein Gate falsifiziert (rot blockt), verifiziert nie vollständig (Rice/Dijkstra). Grün ≠ korrekt.
  • Nur die formalisierbare Klasse — UX, Geschmack, Architektur bleiben menschlich.
  • Der Mensch setzt + verantwortet die Invariante. Eine falsche Spec fängt kein Gate.
  • N=2 Fallstudien, Forschungsprototyp. Steht mit der Skepsis — eine Schraube weiter, nicht „gelöst".

Selbst sehen

git clone github.com/Koschnag/cong-driven-development
dotnet test tests/Cdd.Tests        # 42/42 grün

koschnag.github.io/cong-driven-development — Einstieg · Live-Demo · Code · Paper

Danke. Fragen?