MEASURED
Finding · verify
A language-model judge scored 8 out of 10 on decisions that a solver proved violated the encoded policy.
- The system said
- Judge: PASS, 8 of 10, three seeds.
- The evidence showed
- Z3 proved the decision violated the encoded policy. The judge passed 4 of the 6 violating decisions; the checker caught 6 of 6.
§ 1
The record
FINDING · judge-passed-checker-proved-violationverify · self certification
A language-model judge scored 8 out of 10 on decisions that a solver proved violated the encoded policy.
- Claim
- In the complete rerun, six single-decision cases violated an encoded governance property. The language-model judge passed 4 of the 6 across three seeds each; the formal checker proved the violation in 6 of 6, and both verdicts are sealed in the same record.
- Status
- MEASURED Empirical, with a stated sample.
- Question
- Passed is not correct
- Subject
- An evaluation harness for governed agent decisions built for the study (authored), with a local 14B judge. built for the study
- Frame
- Sixteen sealed records from one rerun (2026-07-20); six violating single-decision cases; three judge seeds per case.
- Method
- Each checkable property is routed to the checker whose logic fits it (Z3 for one decision, Lean 4 for a trace, TLA+ for interleavings, CryptoVerif for authorisation) and the judge's score is sealed beside the proof so the two can be compared.
- Oracle
- The formal checker's verdict against the encoded property; CI checks the headline counts (6 violating cases, judge passed 4, checker proved 6).
- Negative control
- Present Six non-violating rows in the same run where judge and checker agree, so the split is not the judge failing everything; planted-adversarial and model-authored decision sources are reported separately.
- Denominator
- 4 of 6 violating decisions passed by the judge; 6 of 6 proven violated by the checker; 3 seeds each.
- Limitation
- The judge is qwen2.5-coder:14b, a local model, not a frontier judge, and on model-authored rows it grades its own output. A stronger judge may do better; that is unmeasured. The harness depends on two packages that are not yet published on their own, vendored with provenance. Six cases is a demonstration of the split, not a rate.
- Source
- repowazdogz-droid/proof-carrying-evals @ f22def1
- Reproduce
python3 scripts/verify_records.py
- Independent reproduction
- None known.
§ 2
Where this sits
This finding answers Passed is not correct and supports the VERIFY stage of the operating method. It is an instance of the self certification mechanism.