Lernleitfaden: Anwendungsteil 4. LLM-Duell: Verifikator gegen Implementor in formalen Aussagen

Thema: Praktischer Teil 4. LLM-Duell: Verifikator gegen Implementor in formalen Aussagen

Schwierigkeitsgrad: Mittelstufe

Geschätzte Studienzeit: 6-8 Stunden (Theorie + Praxis + Übertragung in Capstone)

Voraussetzungen: Abschluss von Teil 9 des ersten Bandes: überprüfbare Fakten und Spezifikation leitet, Fakten ermöglichen Zusammenführung

Abschluss von Teil 16 des ersten Bandes: unabhängige Überprüfung des Faktenpakets durch Menschen

Grundlegende Vertrautheit mit JSON Schema und dem Given/When/Then-Format

Fähigkeit, Python-Skripte aus der Kommandozeile auszuführen

Verständnis der Grundlagen des Autoscalings in Kubernetes (Repliken, Kontingente, Limits)

Lernziele: Inzident-Szenarien im strengen Given/When/Then-Format formulieren und mit JSON Schema verknüpfen

Minimale Gegenbeispiele konstruieren: Eingaben, die dem Schema entsprechen, aber die Then-Aussage verletzen

Das LLM-Duell-Protokoll Verifikator↔Implementor implementieren mit Dokumentation der Ergebnisse in validation.md

Gefundene Gegenbeispiele in überprüfbare next_guard-Regeln für CI-Pipeline umwandeln

Betriebsgrenzen (Kontingent, Limit, Auswirkungsradius) aus mündlichen Absprachen in formale Spezifikation überführen

Übersicht: Dieses Kapitel lehrt, formal korrekte aber gefährliche Anfragen durch wettbewerbsbasierte Validierung in handhabbare, überprüfbare Regeln zu verwandeln. Das zentrale Szenario ist autoscale_200pct: Ein Webhook fordert 200% mehr Repliken an, aber das Kontingent erlaubt nur 3, und das Limit liegt bei 15. Statt mitten in der Aktion mit einem Fehler abzubrechen, muss das System entweder den Schritt sicher begrenzen oder mit Diagnose ablehnen.

Die LLM-Duell-Technik beauftragt zwei Rollen mit einem dateibasierten Streit: Der Verifikator sucht das minimale Gegenbeispiel, der Implementor repariert Regel und Implementierung. Der Streit endet, wenn das Gegenbeispiel Teil der Spezifikation wird und der erneute Durchlauf PASS ausgibt. Dies ist weder Giftspezifikation (Kapitel 2) noch Mutationstesten (Kapitel 5) — es ist die Prüfung der Robustheit einer bereits formulierten Regel gegen konkrete verletzende Eingaben.

Das Studienminimum zeigt, wie ein Gegenbeispiel in einen überprüfbaren Bescheid wird. Der vollständige Production-Track ergänzt Modellrotation, Ebenen und einen externen Koordinator — dies ist Stoff von Teil 8.

Schlüsselkonzepte: Gegenbeispiel: Minimale Eingabe, die JSON Schema erfüllt, aber die Then-Aussage verletzt. Für autoscale_200pct: current_replicas=12, remaining_quota=3, scale_up_percent=200. Minimalität bedeutet, dass das Entfernen eines beliebigen Feldes die Verletzung zerstört. Das Gegenbeispiel wird als counterexample.json mit den Feldern given_snapshot, when_payload, assertion_id, minimality_trace veröffentlicht.

Verifikator: Rolle, die das minimale Gegenbeispiel für eine Then-Aussage sucht. Gewinnt, wenn ein gültiges minimales Gegenbeispiel konstruiert wird: erfüllt die Eingangsschemata, verletzt aber Then. Erklärt nicht, sondern demonstriert — durch reproduzierbare Eingabe.

Implementor: Rolle, die Code und Regel nach dem Scheitern des Duells repariert. Gewinnt nur unter zwei Bedingungen: Code und Regel sind aktualisiert; der erneute Duell-Durchlauf findet dieselbe Fehlerklasse nicht mehr und bricht bestehende Invarianten nicht. Ist verpflichtet, vier Artefakte auszugeben: repair.patch, schema_delta, rationale, affected_assertions.

Minimalität des Gegenbeispiels: Anforderung, genau die Felder und Werte zu enthalten, ohne die die Verletzung verschwindet. Schlecht: Rauschfelder cluster_id, labels, annotations, node_pool, region — bei der Korrektur ist unklar, was Then bricht. Gut: nur current_replicas, remaining_quota, scale_up_percent.

Betriebsgrenzen: Überprüfbare Beschränkungen, die die Spezifikation von der logischen in die betriebliche Ebene überführen: Kontingent (quota), Frequenzbegrenzung (rate-limit), Auswirkungsradius (blast-radius), Deduplizierung, Wiederholungsfenster, maximale Änderungsgröße. Werden Teil von Then: target_replicas <= max_replicas, executed_delta <= remaining_quota / pod_cpu.

Next guard: Neue Regel, die bei zukünftigen Durchläufen überprüft werden muss. Formuliert im Given/When/Then-Format. Beispiel: „Wiederholter Webhook innerhalb von 2 Sekunden erhöht executed_delta nicht“. Verwandelt einen Einzelfall in einen Präzedenzfallkatalog für CI-Regression.

Validation.md: Duell-Journal, das die Beweiskette speichert: duel_id, assertion_id, fehlschlagender Fall, Spezifikationsversion vor der Korrektur, JSON Schema-Änderung, Code-Änderung, neuer Bescheid, Link zum bestandenen Duell-Test. Kein freier Kommentar im Ticket, sondern reproduzierbares Regressions-Asset.

JSON Schema als Vertrag: Das Schema begrenzt den zulässigen Eingaberaum und verknüpft Given/Then-Felder mit Typen und Beschränkungen. Nach dem Gegenbeispiel ist der Implementor verpflichtet, nicht nur den Code, sondern auch das Schema zu ändern — sonst passieren ähnliche Fehler weiterhin.

Koordinator: Schiedsrichter, der hinzugezogen wird, wenn Verifikator und Implementor nach einer festgelegten Anzahl von Runden nicht übereinkommen. Setzt DEFERRED und leitet in manual-review mit expliziter Beschreibung des strittigen Invariants über. Verhindert endlose Diagnoseschleifen.

Replay benachbarter Fälle: Nach der Korrektur ist der Verifikator verpflichtet, nicht nur das ursprüngliche Gegenbeispiel, sondern auch äquivalente Fälle erneut durchzuspielen: fehlende cluster_id, Null-Kontingent, wiederholter Webhook, remaining_quota=1 bei current_replicas=max_replicas, Konflikt soft_clamp mit blast_radius_limit. Schützt vor schmalem Flicken.

Übungsaufgaben: Titel: Offline-Duell autoscale_200pct starten

Problem: Wechseln Sie in das Verzeichnis book2/examples/tribunal und führen Sie das Skript run_duel.py mit den angegebenen Parametern aus. Finden Sie in der Ausgabedatei out/duel.json den Eintrag für autoscale_counter_200pct. Bestimmen Sie: welche assertion_id geprüft wurde, welcher Bescheid erzielt wurde, welcher allowed_delta-Wert tatsächlich angewendet wurde, welcher diagnostic_code ausgegeben wurde.

Lösung: 1. cd book2/examples/tribunal

1. python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json
2. Öffnen Sie out/duel.json, finden Sie das Objekt mit counterexample_id: "autoscale_counter_200pct"
3. Prüfen Sie die Felder: assertion_id muss "allowed_delta_within_quota" sein, verdict — "PASS"
4. In actual finden Sie: allowed_delta: 3 (durch Kontingent begrenzt), diagnostic_code: "QUOTA_EXCEEDED_AFTER_CLAMP"
5. Stellen Sie sicher, dass die Eingabe dem Schema entspricht (scale_up_percent=200 im Bereich 1-1000), aber Then durch Begrenzung erfüllt wird, nicht durch vollständige Erfüllung der Anfrage

Schwierigkeit: Anfänger

Titel: Minimalität des Gegenbeispiels prüfen

Problem: Gegebenes Gegenbeispiel: {current_replicas: 12, remaining_quota: 3, pod_cpu: 1, scale_up_percent: 200, cluster_id: "agentclinic-prod", namespace: "appointments", labels: {team: "platform"}, node_pool: "standard", region: "us-east-1"}. Kürzen Sie auf das Minimum. Erklären Sie, warum entfernte Felder die Verletzung nicht beeinflussen, und formulieren Sie das Minimalitätskriterium für Ihren Fall.

Lösung: 1. Entfernen Sie cluster_id — Verletzung bleibt (Kontingentprüfung hängt nicht von Cluster-Identifikator ab)

1. Entfernen Sie namespace, labels, node_pool, region — Verletzung bleibt
2. Entfernen Sie pod_cpu — Verletzung verschwindet: ohne pod_cpu ist floor(remaining_quota / pod_cpu) nicht berechenbar, die allowed_delta-Formel bricht
3. Minimales Gegenbeispiel: {current_replicas: 12, remaining_quota: 3, pod_cpu: 1, scale_up_percent: 200}
4. Minimalitätskriterium: Entfernung eines beliebigen der vier Felder macht die Verletzung nicht reproduzierbar

Schwierigkeit: Mittelstufe

Titel: Formulierung von next_guard für high_memory_usage

Problem: Übertragen Sie das Prinzip von autoscale_200pct in das Capstone-Projekt. Szenario: Bei high_memory_usage erlaubt die Regel restart_pod einen Dry-Run, wenn readiness >= 23/25. Aber ein Stateful-Pod mit backup_verified=false darf nicht neu gestartet werden, selbst bei readiness=24/25. Konstruieren Sie ein minimales Gegenbeispiel und formulieren Sie next_guard im Given/When/Then-Format.

Lösung: 1. Minimales Gegenbeispiel: readiness=24/25, stateful=true, backup_verified=false

1. Minimalitätsprüfung: Entfernung von stateful=true — Verletzung verschwindet (readiness >= 23/25 erlaubt Dry-Run); Entfernung von backup_verified=false — Verletzung verschwindet (stateful=true + backup_verified=true zulässig); Entfernung von readiness=24/25 — Verletzung verschwindet (bei readiness < 23/25 ist Dry-Run sowieso blockiert)
2. next_guard-Formulierung: "Given stateful=true und backup_verified=false When readiness >= 23/25 Then dry-run blockiert mit Diagnose STATEFUL_BACKUP_REQUIRED"
3. Eintrag in validation.md:

duel_id: duel-high-memory-001 assertion_id: HM-READINESS-01 counterexample: "readiness=24/25, stateful=true, backup_verified=false" verdict: PASS next_guard: "Given stateful=true und backup_verified=false When readiness >= 23/25 Then dry-run blockiert mit Diagnose STATEFUL_BACKUP_REQUIRED"

Schwierigkeit: Mittelstufe

Titel: Fehleranalyse der Prozedur: nur Code, ohne Schema

Problem: Der Verifikator hat das Gegenbeispiel autoscale_200pct gefunden. Der Implementor änderte nur den Code, fügte die Formel allowed_delta in die Python-Funktion ein, aktualisierte aber JSON Schema nicht — die Felder max_actions_per_window und clamp_policy blieben außerhalb von required. Eine Woche später kam ein neuer Webhook mit fehlendem clamp_policy, das System stürzte mit Fehler ab. Wo liegt der Fehler in der Duell-Prozedur? Welches Artefakt hat der Implementor nicht ausgegeben?

Lösung: 1. Fehler: Der Implementor verletzte die Siegbedingung — er aktualisierte nicht die Regel (Spezifikation und Schema), sondern änderte nur den Code

1. Fehlendes Artefakt: schema_delta — Änderung von JSON Schema, das neue Felder der Antwortpolitik verankert hätte
2. Warum das wichtig ist: Das Schema ist der vor Ausführung prüfbare Vertrag. Ohne Schema passiert die Validierung für neue Eingaben mit fehlendem clamp_policy, und es bricht zur Laufzeit
3. Korrekte Prozedur: Der Implementor muss repair.patch (Code), schema_delta (Schema), rationale (Begründung), affected_assertions (Liste betroffener Aussagen) ausgeben
4. Der erneute Durchlauf muss den benachbarten Fall einschließen: fehlendes clamp_policy, Konflikt soft_clamp mit blast_radius_limit

Schwierigkeit: Fortgeschritten

Titel: Aufbau einer CI-Pipeline mit Duell

Problem: Formulieren Sie die Befehlssequenz für eine CI, die: (1) das Schema validiert, (2) das Duell mit Limit von 8 Runden startet, (3) die Anwesenheit von next_guard in validation.md fordert. Erklären Sie, warum der dritte Schritt — lint_validation.py — notwendig ist, und was passiert, wenn der Verifikator mitten im Sprint ein neues Gegenbeispiel findet.

Lösung: 1. Schritt 1: python3 scripts/spec_ci/lint_spec.py spec/incident-autoscale.md — prüft Syntax und Feldverknüpfung mit JSON Schema

1. Schritt 2: python3 scripts/tribunal/run_duel.py --scenario autoscale --case autoscale_counter_200pct.json --max-rounds 8 --out .artifacts/duels/autoscale.json — startet Duell mit Rundenbegrenzung
2. Schritt 3: python3 scripts/spec_ci/lint_validation.py validation.md --require next_guard — prüft, dass jeder Fehler ein überprüfbares next_guard-Regel erzeugt hat
3. Warum lint_validation.py: Ohne es bleibt das Gegenbeispiel in out/duel.json — einem lokalen Artefakt — und verwandelt sich nicht in ein Regressions-Asset. Die CI blockiert nicht die Wiederholung derselben Fehlerklasse
4. Wenn der Verifikator im Sprint ein neues Gegenbeispiel findet: Die Pipeline muss schema_delta, Regelaktualisierung, erneuten grünen Durchlauf fordern. Roter Status allein reicht nicht — es braucht eine reproduzierbare Spur in validation.md

Schwierigkeit: Fortgeschritten

Fallstudien: Titel: AgentClinic-production: autoscale_200pct und Kontingentfehler

Szenario: Im Cluster AgentClinic-production läuft der Dienst appointments-api. CPU-Auslastung 98%, 12 Repliken, Kontingent erlaubt 3 weitere, Replik-Limit bei 15. Ein Webhook von Grafana kommt an: „Erhöhen Sie die Replikenzahl um 200%“. Formal ist die Anfrage korrekt — alle Felder ausgefüllt, Bereiche gültig. Die Ausführung erfordert 12 zusätzliche Repliken (200% von 12), aber das Kontingent ist 3, und das Limit ist 15.

Herausforderung: Zwei Reaktionsszenarien: (1) Die Regel prüft nur die formale Korrektheit der Eingabe — der Autoscaler bricht mitten in der Aktion mit Fehler ab, hat teilweise Repliken erstellt und Konsistenz verletzt; (2) Die Regel enthält keine Betriebsgrenzen in Then — Kontingent, Limit, Auswirkungsradius gelten als „offensichtlich“ und werden nicht formal geprüft. Das Team stellt fest, dass dieselbe Fehlerklasse bei verschiedenen Eingaben wiederholt auftritt: Null-Kontingent, max_replicas=current_replicas, doppelter Webhook.

Lösung: Implementierung des LLM-Duells Verifikator↔Implementor. Der Verifikator konstruiert das minimale Gegenbeispiel: current_replicas=12, remaining_quota=3, scale_up_percent=200. Der Implementor antwortet mit der Formel allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas) und der Politik hard_block | soft_clamp. Schlüsselschritt: Die Formel wird in JSON Schema durch neue Felder max_actions_per_window und clamp_policy verankert, die required werden. Der erneute Duell-Durchlauf umfasst benachbarte Fälle: fehlende cluster_id, Null-Kontingent, wiederholter Webhook innerhalb des Deduplizierungsfensters, remaining_quota=1 bei current_replicas=max_replicas. Jeder Fehler und Sieg wird in validation.md mit duel_id, assertion_id, next_guard dokumentiert.

Ergebnis: Das System wechselt vom Modus „auf Produktion brechen“ zum Modus „mit Diagnose ablehnen vor Zustandsänderung“. Das Gegenbeispiel autoscale_counter_200pct erhält verdict PASS mit diagnostic_code QUOTA_EXCEEDED_AFTER_CLAMP und allowed_delta=3. Ein neuer Webhook mit denselben Parametern wird in 50 ms mit klarer Diagnose verarbeitet, ohne Teiländerungen. Die CI-Pipeline blockiert Regression: Wenn neuer Code die alte Regel ohne clamp_policy zurückgibt, meldet lint_validation.py einen Fehler. Das Team sammelt 12 Einträge in validation.md pro Quartal, die Kontingent-, Frequenz- und Deduplizierungsfehler abdecken.

Gelernte Lektionen: Minimales Gegenbeispiel ist wertvoller als Erklärung: es ist reproduzierbar und automatisch prüfbar

Betriebsgrenzen müssen in Then stehen, nicht in mündlichen Absprachen — sonst entdeckt jeder neue Ingenieur sie neu

Der Implementor muss das Schema zusammen mit dem Code ändern: schema_delta ist keine Option, sondern Siegbedingung

Benachbarte Fälle im Replay schützen vor schmalem Flicken, der ein Beispiel schließt und einen äquivalenten Fehler offenlässt

validation.md verwandelt einen Einzelfall in einen Präzedenzfallkatalog, den die CI für Regressionsschutz nutzt

Verwandte Konzepte: Gegenbeispiel

Verifikator

Implementor

Minimalität des Gegenbeispiels

Betriebsgrenzen

next_guard

validation.md

Replay benachbarter Fälle

Titel: Übertragung des Prinzips in Capstone: high_memory_usage und Stateful-Blocker

Szenario: Der Student absolviert den Studientrack und muss das Prinzip autoscale_200pct in sein eigenes Capstone-Projekt übertragen. Sein Szenario: Bei hoher Speicherauslastung erlaubt die Regel restart_pod einen Neustart, wenn readiness >= 23/25. Auf Produktion stellt sich heraus, dass ein Stateful-Pod mit ungeprüftem Backup (backup_verified=false) bei readiness=24/25 neu gestartet wird und Zustand verliert.

Herausforderung: Der Student kopiert das Gegenbeispiel autoscale_200pct anstatt das Prinzip zu formulieren. In capstone/validation.md erscheint ein Eintrag über current_replicas und remaining_quota — Felder, die für restart_pod irrelevant sind. Der Reviewer lehnt ab: Gegenbeispiel nicht minimal, next_guard nicht auf Domäne anwendbar. Ein eigenes minimales Gegenbeispiel muss konstruiert und next_guard formuliert werden, wobei Struktur beibehalten, aber Inhalt geändert wird.

Lösung: Analyse der Struktur aus autoscale_200pct: Minimales Gegenbeispiel enthält nur Felder, ohne die die Verletzung verschwindet; next_guard formuliert eine neue Regel in Given/When/Then; Betriebsgrenze überführt Beschränkung von mündlich in überprüfbar. Für high_memory_usage: Minimales Gegenbeispiel — readiness=24/25, stateful=true, backup_verified=false. Minimalitätsprüfung: Entfernung von stateful=true oder backup_verified=false beseitigt die Verletzung. next_guard: „Given stateful=true und backup_verified=false When readiness >= 23/25 Then dry-run blockiert mit Diagnose STATEFUL_BACKUP_REQUIRED". Betriebsgrenze: restart_pod wird nicht auf Namespace-Ebene ausgeweitet.

Ergebnis: Der Student erlernt die Übertragung des Prinzips, nicht das Kopieren. Der Eintrag in capstone/validation.md wird vom Reviewer akzeptiert. Bei späterer Ausweitung der Regel auf Namespace-Level-Restart erhält der Student automatisch einen Konflikt mit next_guard und ist gezwungen, den Guard entweder explizit abzuschwächen (mit Begründung) oder die Beschränkung beizubehalten. Dies verhindert die implizite Ausweitung des Auswirkungsradius.

Gelernte Lektionen: Übertragung vom Studienfall in Capstone ist Formulierung des Prinzips, nicht Kopieren der Daten

Minimalität wird an Domäne geprüft: für Autoscale ist es Kontingent, für restart_pod ist es stateful + backup

next_guard erzeugt zukünftige Reibung: jede Regelausweitung muss mit der dokumentierten Beschränkung interagieren

Struktur von validation.md ist universell: duel_id, assertion_id, counterexample, verdict, next_guard ist auf verschiedene Domänen anwendbar

Verwandte Konzepte: next_guard

Minimalität des Gegenbeispiels

Betriebsgrenzen

validation.md

Studientipps: Beginnen Sie mit dem Offline-Durchlauf: cd book2/examples/tribunal && python3 scripts/run_duel.py. PASS in stderr zu sehen — ein schneller Erfolg, der motiviert, Details zu verstehen

Lesen Sie die Theorie, nachdem Sie das Skript gestartet und kaputt gemacht haben: Entfernen Sie das Feld clamp_policy aus der Eingabe, sehen Sie, wo genau es bricht — so verstehen Sie, warum das Schema wichtiger ist als der Code

Nutzen Sie die Technik „Rauschfeld“: Fügen Sie dem Gegenbeispiel cluster_id, labels, annotations hinzu — stellen Sie sicher, dass das Duell die Verletzung immer noch findet. Dann entfernen Sie eins nach dem anderen, bis Sie das Minimum finden. Das ist die manuelle Prüfung dessen, was der Verifikator automatisch macht

Führen Sie parallel ein validation.md manuell, vor der Automatisierung: Notieren Sie duel_id, assertion_id, Gegenbeispiel, next_guard auf Papier oder im Editor. Vergleichen Sie mit der Ausgabe von lint_validation.py — verstehen Sie, welche Felder die Maschine streng prüft und welche der Interpretation überlässt

Für visuellen Stil: Zeichnen Sie ein Flussdiagramm mit fünf Schritten (Given/When/Then → Verifikator → Implementor → Replay → validation.md) und hängen Sie es neben den Arbeitsplatz. Gehen Sie bei jedem neuen Inzident danach — Sie entwickeln Muskelgedächtnis

Für auditiven Stil: Sprechen Sie Given/When/Then laut vor, bevor Sie es aufschreiben. Wenn der Satz nicht in drei Zeilen passt — ist die Spezifikation noch nicht bereit für das Duell

Für kinästhetischen Stil: Modellieren Sie das Duell rollenbasiert mit einem Kollegen. Einer ist Verifikator, sucht Gegenbeispiel, der andere ist Implementor, repariert in 5 Minuten. Timeboxing zeigt, wo die Prozedur stecken bleibt

Vergleichen Sie mit dem Gelernten: Kehren Sie zurück zu Teil 9 (überprüfbare Fakten) und Teil 16 (menschliches Review). Das Gegenbeispiel im Duell ist die automatisierte Review, die vor dem Merge stattfindet, nicht danach

Verschieben Sie Production-Komplexitäten: Modellrotation, Ebenen, Koordinator — Stoff von Teil 8. Jetzt liegt der Fokus auf einer Runde für eine Regel. Nicht zerstreuen

Prüfen Sie sich mit Kontrollfragen am Kapitelende: Warum Minimalität, warum Erklärung nicht Beweis ersetzt, was ändert der Implementor außer Code, wo liegt der Fehler wenn nur Code ohne Schema

Zusätzliche Ressourcen: Examples/tribunal/readme.md: Lokales ausführbares Duell-Analogon mit Startanleitung und erwarteter Ausgabe

Examples/tribunal/specs/autoscale_spec.yaml: Studienspezifikation autoscale mit Given/When/Then und JSON Schema

Examples/tribunal/cases/autoscale_counter_200pct.json: Minimales Gegenbeispiel für den Durchlauf

Examples/tribunal/scripts/run_duel.py: Offline-Duell-Skript für das Studiendurchlauf

Book/part-09-feature-validation.md: Überprüfbare Fakten und „Spezifikation leitet, Fakten ermöglichen Zusammenführung"

Book/part-16-team-code-review.md: Unabhängige Überprüfung des Faktenpakets durch Menschen

Github spec kit: https://github.com/github/spec-kit — Praxis des specification-first in SDD

Wikipedia: formal specification: https://en.wikipedia.org/wiki/Formal_specification — Given/When/Then als formale Spezifikation

Judgment.example.md: Beispiel der Bescheid-Gestaltung mit Abstimmung von counterexample_id und assertion_id

Zusammenfassung: Das LLM-Duell Verifikator↔Implementor verwandelt die formale Spezifikation in einen handhabbaren Mechanismus zur Prüfung inzidenter Entscheidungen. Das Schlüsselergebnis ist keine abstrakte Textprüfung, sondern ein funktionierendes Protokoll aus vier Schritten: Inzident-Szenario ist mit JSON Schema verknüpft, strittige Bedingungen sind mit minimalen Gegenbeispielen geprüft, Betriebslimits sind Teil der Spezifikation geworden, jeder Fehler ist als reproduzierbare Verbesserung in validation.md dokumentiert.

Der Hauptwert liegt in den Betriebsgrenzen. Kontingent, Frequenzbegrenzung, Auswirkungsradius werden aus mündlichen Absprachen in überprüfbare Then-Aussagen überführt. Automatische Remediation ersetzt nicht die Sicherheit durch formal korrektes, aber gefährliches Handeln.

Das Studienminimum erfordert drei Artefakte: Given/When/Then-Szenario, verknüpft mit Schema; minimales counterexample.json oder Eintrag in validation.md; formuliertes next_guard im Given/When/Then-Format. Der vollständige Track ergänzt repair.patch, schema_delta, Matrix benachbarter Gegenbeispiele und lokalen smoke-pass.

Übertragung in Capstone ist Formulierung des Prinzips, nicht Kopieren. Aus autoscale_200pct wird die Struktur der Minimalität und next_guard genommen, der Inhalt wird für die Domäne high_memory_usage oder das eigene Projekt gebaut.