Artifact
proof-carrying-evals
Governance properties routed to the checker whose logic fits, with the LLM judge's score sealed beside the proof.
What it establishes
That an evaluation harness can route each checkable governance property to a formal checker (Z3 for one decision, Lean 4 for a trace, TLA+ for interleavings, CryptoVerif for authorisation) and keep the language-model judge's opinion labelled as an opinion, so that on the six violating cases the judge's 4 of 6 passes and the checker's 6 of 6 proofs sit in one record.
What it does not establish
That a frontier judge would fail the same way; the judge is a local 14B model and sometimes grades its own output. Two dependencies are not yet published on their own and are vendored with provenance.
Method
Sixteen sealed records from one complete rerun; model-authored and planted-adversarial decisions reported separately; CI recomputes the headline counts.
Results
Judge passed 4 of 6 violating decisions; checker proved 6 of 6; on six non-violating rows both agree.
What has to be trusted
Z3, Lean 4, TLC and CryptoVerif and each encoding; the vendored omega_seal and omega_gate packages; the local judge model.
Prior work
LLM-as-judge evaluation and formal runtime verification. The contribution is the routing by property kind with both verdicts sealed together.
Reproduce it
python3 scripts/verify_records.py
Findings drawn from this artifact are on the evidence ledger.