How the pieces fit

Ten artifacts, one trust boundary. This page is the map: what each piece does, what depends on what, and — the part that matters — which side of the boundary each one sits on.

The trust boundary

  UNTRUSTED                          |  TRUSTED (and small enough to read)
  ---------------------------------- | ----------------------------------
  whatever produced the certificate  |  certkit          ~30 lines of arithmetic
    a solver, an LP, a model, you    |  certkit-js       the same, written separately
                                     |
  the specification                  |  <- NOT trusted by the checker, but not
    (a human wrote these relations)  |     checked by it either. See below.

The checker trusts nothing the certificate says: it rebuilds every obligation from the specification and ignores any atoms the certificate carries. What it cannot do is tell you the specification describes your program. That is the one assumption the whole system rests on, and it is why specs are kept to a handful of readable relations.

Dependency direction

  certkit  (no dependencies, standard library only)
     ^
     |-- exploit-counter   uses certkit's atom type; adds exact counting
     |        ^
     |        |
     |-- crs-mcp           wraps both, exposes them to agents
     |
     |-- certkit-action    runs the CLI in a workflow
     |
  soundnessbench           deliberately does NOT import certkit
                           (it has to be able to grade certkit)

  certkit-js               shares NO code with certkit, by construction

The two non-arrows are the interesting ones. soundnessbench computes its ground truth by its own exhaustive enumeration, with its own atom representation, because a benchmark that imported the tool it grades would be measuring agreement rather than correctness. certkit-js is a separate implementation for the same reason: two programs that share no code agreeing on 246 vectors is evidence; one program agreeing with itself is not.

Inside certkit

Module	Role	Trusted?
`atoms.py`	The one canonical relation shape: `sum(c*v) + k <= 0`. Exact rationals.	yes
`farkas.py`	The refutation check itself. No search, no solver, no floats.	yes — this is the core
`cert.py`	Reconstruction, fingerprint binding, the three verdicts.	yes
`report.py`	Every output format from one place, so a refusal is worded identically everywhere.	presentation
`schemas/`	JSON Schema for both formats, so other tools can emit them.	data
`smtlib.py`	Export is total; import is deliberately partial and refuses by name.	bridge
`scaffold.py`, `explain.py`	Authoring and prose. Never change a verdict.	convenience
`lsp.py`, `notebook.py`, `precommit.py`	Frontends. Each re-uses the same verdict; none of them softens it.	frontend

The rule for everything below cert.py: a frontend may change how a verdict is displayed and may never change what it is. That is enforced by tests rather than by convention — the notebook renderer, the SARIF output, the JUnit output, the LSP diagnostics and the pre-commit hook each have a test asserting that UNVERIFIED does not render as a pass.

Where the expensive work happens

Checking is linear in the size of the obligation and takes microseconds. The costly parts of the toolkit are elsewhere, and each is capped rather than allowed to degrade:

exploit-counter enumerates a declared box exactly. The cap applies to the enumerated product, not the box volume, and exceeding it is a refusal with a reason — never a silently sampled answer presented as exact.
soundnessbench brute-forces every task's answer. That is why the boxes are small, and why the answers ship precomputed, keyed by a content hash of the relations so an edited task cannot be served a stale answer.

Caches, and why they cannot go stale

Two caches ship as committed data files: the benchmark's ground truth, and the minimal-break offsets its hard split needs. Both are keyed by a hash of the relations they answer. Editing a task changes the key, misses the cache, and recomputes. Staleness is not detected — it is unreachable, which is a different and much stronger property.

Every other cache in the toolkit is in-process and keyed by input: the suite memo, and the schema loader. A test asserts that a mutated task produces a different key, so the property is checked rather than asserted.

The three data artifacts

cve-proof-corpus — six real vulnerability classes: the relation each check turned on, in words and in atoms, with a certificate that re-verifies from the published file.
soundnessbench tasks — synthetic families plus a hard split derived from the corpus. Ground truth by enumeration, always.
certkit-js vectors — 246 spec/certificate pairs with the verdict CPython reached, replayed by the JavaScript implementation in CI.

Each is generated by a committed script, and CI regenerates and compares rather than trusting the file.