Technischer Überblick · für Entscheider & Architekten

CDD — wie es funktioniert

Diszipliniertes KI-Coding: ein Loop mit einem fälschungssicheren Terminierungs-Orakel. F#/.NET, Open Source.

Cong Chanh Vinzenz Nguyen · ohne tiefen Formalismus — Tiefe steht im Paper

Der Loop und sein blinder Fleck

Agentic Coding = die KI in einer Schleife, die sich selbst nachbessert (z. B. „Ralph": while :; do cat prompt | claude; done).

  • Der Motor (Brute Force + Persistenz) ist die leichte Hälfte.
  • Die schwere Hälfte: Woran terminiert er? „Agent sagt fertig" / Exit-0 / selbst geschriebene Tests sind kein verlässliches Orakel.

Der Kern: Generator ⊥ Orakel

Generator

schreibt Code + Tests. Per Werkzeug-Allowlist kein Schreibrecht aufs Gate — kann sich kein „grün" geben.

Orakel

prozess-extern, entscheidet „fertig". Getrennt vom Generator → kein korreliertes Selbst-Benoten (vgl. VeriAct).

Die Trennung mildert Common-Mode-Fehler — sie eliminiert sie nicht (gleiche Kriterienquelle bleibt ein Restrisiko).

Die Referenz: der SPOT-Graph

Ein getypter F#-Discriminated-Union-Graph als Single Point of Truth — ein git-versioniertes JSON pro Knoten.

  • Knoten: Spec (Given/When/Then), Test, Risk, Component, Invariant, Begriff, ADR …
  • Konvergenz je Knoten: Aligned · Pending · Diverged · Orphaned.
  • Die Spec ist zugleich externalisiertes Systemwissen — gegen Blackbox/Cognitive Debt.

Der Fluss: Spec → Test → Code

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

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

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.

setzeAlignedWennGruen: Aligned NUR wenn (Marker abgedeckt) UND (echter Lauf grün)
  istGruen = passed > 0 && failed = 0     # „No test" ist nicht grün
  gateGruen = istGruen && keine Validate-Fehler

Maschinell getestet — eine FsCheck-Property beweist: ein nicht-grüner Lauf macht einen Knoten nie Aligned. Kein erschlichenes Grün.

Drei Verifikationsschichten

Typen

illegale Zustände unrepräsentierbar (F#-DUs) — der Compiler als Mini-Gate.

FsCheck-Property

eine Eigenschaft über unbeschränkte Eingaben statt Beispieltabelle.

Lean-4-Beweis für die tragenden Invarianten (Werterhaltung, Nichtnegativität): bewiesen für jeden Fall, sorry-frei. Die Kette Typen → Property → Beweis — abgestuft nach Wichtigkeit.

Ralph × CDD: der Loop bekommt sein Orakel

PRE-LOOP (Mensch):   Domänenwissen → SPOT-Spec + Invarianten (die eigentliche Arbeit)
LOOP-TICK:           Plan-Injektion → Generator-Tick → GATE (Validate → dotnet-test → Marker)
TERMINIERUNG:        alle Ziel-Knoten Aligned (gemessen), NICHT „Agent sagt fertig"
                     harte max-attempts NUR als Token-Notausgang

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), es verifiziert nie vollständig (Rice/Dijkstra). Grün = „die Tests passen", nicht „korrekt".
  • Nur die formalisierbare Klasse — UX/Architektur/Geschmack sind nicht konvergierbar.
  • Der Mensch setzt + verantwortet die Invariante. Eine falsche Spec fängt kein Gate.
  • N=2 Fallstudien, Forschungsprototyp. Terminierung ≠ garantierte Lieferung.

Reproduzieren & selbst sehen

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

Ein-Klick im Browser: Open in Codespaces · Quick Guide & Belege auf koschnag.github.io/cong-driven-development

Fragen?