Ein AI-natives Entwicklungs-Framework, in dem Review zur Konvergenz gegen eine externalisierte, getypte Spezifikation wird — nicht der Diff, den ein Mensch liest und glaubt.
Die Skeptiker haben recht — Voll-Automation ist Hype. Trotzdem lässt sich eine Schraube weiterdrehen.
Die Grenze der KI-Software-Automation ist das Setzen der Invariante: im System nicht selbst-fundierbar (ein Regress, der nur an einem Anker außerhalb des Prüfvorgangs terminiert), und dass der Mensch ihn setzt, ist eine Wahl — kein Penrose-Lucas.
Alles danach kann die Maschine prüfen, wenn die Architektur stimmt: Der KI-Generator kann per Werkzeug-Allowlist keinen Code schreiben; das Orakel bindet Aligned an einen im Testcode abgedeckten Test, dessen Greenness die CI-Suite erzwingt (rot blockt den Merge) — Test-PASS, nicht bloßer Exit-0. Genau das unterscheidet es von Kiro oder GitHub Spec Kit, wo dasselbe System Spec, Code und Test erzeugt.
Das Projekt nutzt ein paar Werkzeuge aus der funktionalen/formalen Ecke. Kurz übersetzt, je mit Java-Analogie.
Funktionale Sprache auf .NET (dieselbe Runtime wie C#). Immutable by default, Pattern Matching, knappe Typen.
≈ Java mit record + sealed + Pattern-switch — aber durchgängig und kürzer.
Ein Typ, dessen Wert genau einer von mehreren Fällen ist (Summentyp). Der SPOT-Graph ist so getypt: Spec | Test | Risk | Component …
≈ Java sealed interface + records + erschöpfendes switch.
Ein Theorembeweiser: man formuliert einen mathematischen Satz, der Compiler prüft den Beweis. Anders als Tests (Stichproben) gilt ein Beweis für alle Fälle.
≈ Java kein echtes Pendant; am nächsten: Dafny / JML+KeY.
sorry ist Leans Platzhalter „Beweis hier ausgelassen" — eine Lücke, die trotzdem kompiliert (wie ein // TODO, das durchwinkt). sorry-frei = keine einzige Lücke; #print axioms listet die Grundannahmen, bei uns nur Standard (propext, Quot.sound), keine Schummel.
Statt fester Beispiel-Eingaben generiert das Framework hunderte Zufallseingaben und prüft eine Eigenschaft; schlägt sie fehl, „shrinkt" es auf das kleinste Gegenbeispiel.
≈ Java jqwik (bzw. QuickCheck).
Der Schritt, der entscheidet „fertig/korrekt?". Hier: ein Knoten wird nur Aligned, wenn ein echter Test grün ist — nicht weil „der Agent sagt fertig".
Single Point of Truth — der eine getypte Graph, der Spec, Test, Risiko, Komponente … als Knoten hält. Ein JSON pro Knoten, git-versioniert, diffbar.
Model Context Protocol — die standardisierte Schnittstelle, über die ein KI-Client (z. B. Claude) Werkzeuge aufruft, hier um den SPOT zu lesen/ändern.
≈ Java eine API-Spec für Tool-Calls.
Vom Ein-Klick-Browser bis zum Homelab-Betrieb wie ein Cloud-Programm.
Die echte Cockpit-Oberfläche mit dem realen Self-Modell (66 Knoten) — Diagramm, Formal-Sicht, Konvergenz. Read-only, kein Login, kein Setup.
Ohne Login, ohne Setup: das fälschungssichere Gate zum Anfassen — du wählst, was der Agent schreibt, und siehst das Orakel live entscheiden.
Ein Klick → die echte CLI & das Cockpit laufen im Browser (Cloud-Dev-Umgebung, kein Setup). Schnellster Weg, es laufen zu sehen.
CLI + Cockpit für Linux/Windows/macOS — kein .NET-Runtime nötig. Auspacken, cdd init, los.
Öffentliches Image, SPOT-Root als Volume. Läuft auf jedem Container-Host (x86).
docker compose up mit Reverse-Proxy + Basic-Auth davor — erreichbar wie ein Cloud-Programm.
# Container — Cockpit „Cong OS" auf :8080, SPOT persistent im Volume docker run -d --name cdd -p 8080:8080 -v /srv/cdd/data:/data ghcr.io/koschnag/cdd:latest # Oder lokal mit der CLI ein neues Programm modellieren cdd init # SPOT-Store (.spot/) anlegen cdd derive-tests --write # Spec-Kriterien → Test-Knoten cdd derive-code --out tests/Derived.fs # → F#-Test-Skelette cdd sync-tests --write # Aligned bei abgedecktem Test-Marker; Greenness erzwingt die CI
Zwei öffentliche Fallstudien — CI-grün, in Minuten reproduzierbar. Copy-paste: ein frischer Klon liefert genau diese Zahlen.
# Methode/IDE — erwartet: 42/42 git clone https://github.com/Koschnag/cong-driven-development && cd cong-driven-development dotnet test tests/Cdd.Tests # 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
| Repo | Rolle | Anker | CI |
|---|---|---|---|
| cong-driven-development | Methode / IDE | main | Actions ✓ |
| runenruf | Fallstudie A (Spiel) | 56376a5 | Actions ✓ |
| ledger-casestudy | Fallstudie B (Hauptbuch) | 0f39ab0 | Actions ✓ |
Bewusst getrennte, unabhängige Repos — kein Monorepo. Die Unabhängigkeit ist Teil des Belegs: reproduzierbar aus separaten Quellen, Generator und Prüf-Orakel dekorreliert.
Fallstudie C — Fremdprojekt-Beweis: Prosa → SPOT → Tests → Code → Konvergenz an einem unabhängigen Projekt.
Steuerzentrale / Control Plane: das Programm-Modell über CDD + Runenruf + Fallstudie, mit Live-Konvergenz-Dashboard.
Wissenschaftliche Fallstudie: spec-/modell-/konvergenz-getriebene Entwicklung mit LLMs — Thesis/Paper/Slides aus einem SPOT.
Vom Einsteiger ohne Vorwissen bis zum zitierfähigen Paper.
Agentic Loops & Gates in 2 Minuten, erklärt über CI, Code-Review, TDD und Typen. Wenn du das Thema noch nicht kennst: hier.
Die ganze These als Fließtext mit zwei Diagrammen. Hier anfangen.
Die ausführliche Position: Blackbox-Stack, der Bruch beim Probabilistischen, Determinismus in die Gates, Werkzeugkasten F#/FsCheck/Lean.
Die diagrammreiche, interaktive Tour (14 Folien) mit eingebetteter Live-Demo. Problem → Idee → Gate → Demo → Grenzen.
20 S., arXiv-Stil, A/B-Verifizierbarkeitstabelle, Lean-Listing, 12 verifizierte Zitate.
Die Antwort auf den Loop-Engineering-Diskurs mit Tiefe — deutsch, englisches Abstract.
Was die Arbeit nicht behauptet — im Paper als Klasse B markiert.
Nichts davon musst du mir glauben — alles ist Code, Commit oder reproduzierbarer Lauf.
Cdd.Core.Sync.SetzeSpecAligned (Sync.fs): setzt Aligned bei vorhandenem Test-Marker (covered) — die Greenness sichert die CI, nicht die Funktion.