2.1 Golden unabhängig
PruefaufgabeGolden unabhängig (aus der Spec, NIE aus der RTL)
Beweis-ArtefaktHerkunfts-Notiz im Golden
Das Orakel niemals aus der RTL ableiten - sonst erbt es exakt die Fehler, die es fangen soll. Quelle ist die Spec, sonst nichts.
2.2 self_check() = 0 Fehler
Pruefaufgabeself_check() = 0 Fehler
Beweis-ArtefaktRun-Log Exit 0
Das Orakel beweist sich zuerst selbst (Wahrheitstabelle oder Invariante wie q·d+r=n). Erst Exit 0 mit 0 Fehlern macht Referenz zu Gold.
2.3 Grenzfälle vollständig
PruefaufgabeGrenzfälle + Wahrheitstabelle vollständig
Beweis-ArtefaktVektor-Statistik
Zufall ergänzt, ersetzt nie: alle-0, alle-1, 0xAA/0x55, Einzel-Bits, ungültige Vorbedingungen. Fehler wohnen an den Rändern, nicht in der Mitte.
2.4 Deterministisch: fester Seed
PruefaufgabeDeterministisch: fester, dokumentierter Seed
Beweis-ArtefaktSeed in Datei + JSON
Fester Seed = bit-identische Läufe = jeder Mismatch reproduzierbar. Ein "zufälliger" Fehler ohne Seed ist ein verlorener Fehler.
2.5 Erwartungswert je Testfall
PruefaufgabeJeder Testfall trägt seinen Erwartungswert
Beweis-Artefaktvectors_<block>.json
Die Maschine vergleicht, kein Mensch "schaut drüber". Augen ermüden, Vergleichszähler nicht.