The certificate corpus¶
A specification and a checker are instructions and a tool. Neither is evidence. This corpus is the evidence: real certificates, produced by the engine we ship, for a real policy, published so that you can run the reference checker over them within minutes, with no key, no network and none of our software beyond one Python file.
The policy is a consumer-finance guardrail written against the Financial Conduct Authority's published rules, with its table of obligations: each one an action the policy must never allow without a condition. Every obligation was run through the engine, and the corpus holds what came out.
What it holds¶
- An obligation that holds has two certificates. One comes from the
proofprofile, where a fast decision procedure refutes the bypass and the certificate says so without being able to replay it: the checker reportsnot_self_contained. The other comes from thepatchprofile, where that procedure is off and every step is derived: the checker replays it and reportsverified. Each certificate has its proof in words beside it, and its full result. - An obligation that does not hold has the engine's result, the patch it proposes, the patched policy, the patch's safety proof in words, and the certificate that the patched policy closes the hole, which the checker verifies. Two obligations of this policy do not hold, and they are the reason it is the reference: a corpus of nothing but clean results would show the checker succeeding and nothing else.
- One FRAT-backed refutation, under
FCA-01a/frat/: the certificate, the CNF it was refuted as, and the solver's FRAT log, whichfrat-rselaborates and checks. Its certificate isnot_self_containedto our checker, which does not read FRAT; chapter 7 says what that proof establishes and who checks it.
The expected checker outcome is in the table, so you know before you start which files should report
not_self_contained.
The manifest¶
manifest.json records the SHA-256 of every file, the profile each came from, the
engine that produced them and the policy's provenance:
- The manifest's format:
qls-corpus/1 - The engine, by the commit it was built from (with FRAT):
9a7b248691f9a1f1e60c94a7e7f64cd9504e5a11 - The run's date: 2026-10-13
- The profiles used:
patch,proof - The run's environment:
OMP_NUM_THREADS=1 - 86 files, each with its SHA-256
- The policy's provenance: Written by Stalwart from the Financial Conduct Authority's published rules it cites (the Consumer Duty, COBS, MCOB and the financial promotion rules); no clause derives from a customer's material. (Stalwart Technologies Ltd)
The engine ran on one thread. Run on several, it builds a derivation's rows in whatever order its threads finish, and a certificate is as valid either way but its bytes differ; one thread makes every byte reproducible, so a changed certificate means a changed engine. The corpus is regenerated whenever the engine changes what it writes, and the guide's build fails until it is.
The policy's behavioural test suite is not in the corpus: it drives a hosted model, so its result is not a file the engine can reproduce. The corpus holds what the engine decides.
Checking it¶
Download the files, and the reference checker from the certificate specification, then run it over each certificate:
$ python qls-check.py FCA-01a/patch.certificate.json
qls-check: verified
replayed 105 operation(s), and the withheld final step yields 0 = 1
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
0
$ python qls-check.py FCA-01a/proof.certificate.json
qls-check: not_self_contained
the contradiction rests on rows asserted by cryptominisat-phase0, which nothing in the certificate checks
This establishes that a derivation or a refutation is valid. It does not establish that the policy is safe, nor that the equations are the policy.
$ echo $?
2
The checker's three outcomes, verified, not_self_contained and failed, exit 0, 2 and 1.
stalwart check in the stalwart-agents package runs the same file. A check establishes that a derivation
or a refutation is valid. It never establishes that the policy is safe, nor that the equations are the
policy: chapter 7 is what a certificate establishes and what it does not.
Provenance¶
Only policies the company owns outright are published, and each carries a provenance record in the manifest. Where a clause derives from a customer's material it is replaced before publication with an equivalent drawn from published rules, and the replacement is noted; a policy whose provenance cannot be established is left out rather than sanitised.