certkit

A certificate format for machine-checked program admission, and an independent checker for it.

Try it now, no install: open the browser demo and press Load a forgery — the checker refuses it, client-side.

The checker imports nothing outside the Python standard library. No solver, no search, no floating-point arithmetic. It fits in an afternoon of reading, which is the entire point: you should not have to trust the tool that produced a proof in order to believe the proof.

pip install "certkit@git+https://github.com/nickharris808/certkit@main"

Pre-release. The PyPI name is reserved and publication is imminent; until then the line above is the working install. It is tested in CI on Linux, macOS, and Windows.

30-second quickstart

The example ships inside the package, so this works immediately after pip install — no repository checkout, no files to create:

certkit demo

certkit demo -- CVE-2014-0160 (Heartbleed) shape
  claim: guard `19 + payload <= record_len`
         implies `3 + payload <= record_len` for payload in [0, 65535]

  valid certificate  -> ACCEPTED
      obligation 0: ok
  forged certificate -> REFUSED
      obligation 0: FAIL -- non-strict combination needs const > 0, got -65535

  As expected: the real certificate checks out and the forgery does not.

To check your own files:

certkit check --spec my.spec.json --cert my.cert.json

New here? TUTORIAL.md walks a real C bounds check all the way to a CI gate in about fifteen minutes — including what it looks like when the guard is wrong.

CLI reference

certkit {check,explain,init,sos,demo}

Command	What it does
certkit demo	Run the bundled Heartbleed example: one valid certificate, one forged. No files needed.
certkit init	Scaffold a spec from written relations, so you never hand-write JSON atoms.
certkit check	Decide a spec/certificate pair. This is the one CI runs.
certkit explain	Print the refutation arithmetic — which atoms, which weights, what cancels.
certkit sos	Check a rational sum-of-squares certificate.
certkit schema	Print the JSON Schema for a format, so other tools can emit it.
certkit export	Emit each obligation as SMT-LIB 2, for z3 / cvc5 / anything else.
certkit import	Read an SMT-LIB 2 script back into a spec (linear integer fragment).
certkit lsp	A language server: diagnostics on spec files, in your editor, as you type.

certkit init

certkit init \
  --domain "0 <= payload" --domain "payload <= 65535" \
  --guard  "19 + payload <= record_len" \
  --safety "3 + payload <= record_len" \
  --name heartbleed -o heartbleed.spec.json

Flag	Meaning
--domain RELATION	A bound on the attacker's inputs. Repeatable.
--guard RELATION	The check your code performs. Repeatable.
--safety RELATION	The property that must hold. Repeatable; one obligation each.
--name, -o/--out	Spec name; output path (stdout if omitted).

Accepts <=, <, >=, >, integer coefficients with *, and +/-. Rejects == (that is two atoms — write both), chained comparisons, and anything nonlinear, rather than guessing. Parsing the relations above reproduces the hand-written bundled spec byte for byte, fingerprint included.

certkit check

Flag	Meaning
--spec, --cert	The pair to check. Required.
--no-fingerprint	Skip the binding check. Can only ever yield UNVERIFIED (exit 3), never ACCEPTED.
--json	Shorthand for --format json.
--format	text, json, sarif, junit, or markdown. See below.

Output formats

certkit check --spec my.spec.json --cert my.cert.json --format sarif > certkit.sarif

Format	For
text	a terminal
json	scripts; the report verbatim, including verdict and binding_verified
sarif	GitHub code scanning — a refusal becomes an alert on the PR
junit	most CI systems render this natively
markdown	a PR comment or job summary

Changing the format never changes the verdict or the exit code. UNVERIFIED is its own level in every one of them — SARIF rule certkit/unverified, a JUnit failure of type unverified — because a format that rendered it as a pass would undo the reason the third verdict exists.

Talking to solvers (SMT-LIB 2)

certkit export writes the obligation domain AND guard AND NOT(safety[i]) as an SMT-LIB script:

certkit export --spec heartbleed.spec.json -o obligation.smt2
z3 obligation.smt2      # unsat
cvc5 obligation.smt2    # unsat

unsat is the same claim an ACCEPTED certificate makes, reached by a completely independent implementation. sat means the guard really does admit a forbidden state, and the model is your counterexample. Both directions are cross-checked over a sweep of guard/safety pairs — if certkit ever accepted something a solver called sat, that test fails. CI runs this against z3 on every push and fails if no solver is present, so the check cannot degrade into a silent skip; a second solver (cvc5) is used as well wherever it is installed, and the two must agree.

Going the other way is deliberately partial:

certkit import --smtlib theirs.smt2 -o spec.json

certkit handles quantifier-free linear integer arithmetic. Anything else — a nonlinear product, a Real or BitVec sort, an uninterpreted function, a quantifier, an equality — is refused with the construct named, rather than dropped:

error: sort 'Real' for 'x': certkit handles Int only (no Real, Bool, or BitVec)
error: nonlinear multiplication: certkit handles linear arithmetic only
error: an equality is two atoms; assert the two inequalities you mean instead

A partial importer that silently ignored what it did not understand would produce a spec proving something weaker than the file said, and everything downstream would then be correct about the wrong theorem. Refusing is the only safe behaviour.

Note also that an SMT-LIB file carries no notion of which relations are assumptions and which is the check, so every assertion becomes a safety conjunct and you move them into domain and guard yourself. That is a modelling decision; guessing it would change what gets proved.

In your editor

certkit lsp        # speaks LSP over stdio; standard library only, no pygls

Point any editor's LSP client at it for *.spec.json and you get diagnostics while you write the guard rather than after CI has stopped you merging. It reports three things: structural problems in the spec, the verdict of checking a *.cert.json sitting beside it, and variables the guard uses that the domain never bounds.

That last one is information, not an error — an unbounded variable makes the claim stronger (the obligation has to hold for every value it could take) and therefore harder to prove, which is the first thing to check when a guard you believe is correct will not verify. The server has no producer in it, so it never offers to "fix" a guard, and it never tells you one is correct: no diagnostics means nothing was found wrong with the file.

In a notebook

CheckReport renders itself in Jupyter — three verdicts, three colours, and UNVERIFIED gets its own rather than being folded into pass or fail. exploit-counter's Decision and OverAcceptance and crs-mcp's Verdict do the same. A notebook is where a result is most likely to be skimmed rather than read, so an abstention that looked like a pass would do the most damage there.

As a pre-commit hook

repos:
  - repo: https://github.com/nickharris808/certkit
    rev: main
    hooks:
      - id: certkit

Every staged *.cert.json is checked against the *.spec.json beside it. A certificate with no spec beside it fails, rather than being skipped — a gate that silently skips what it cannot check reports "all certificates verified" while verifying none. UNVERIFIED blocks the commit too: in a gate, "declined to certify" and "refused" have the same consequence.

ci-templates/ has the same job for GitLab CI and CircleCI, both emitting JUnit their UI renders natively.

Emitting certkit from your own tool

certkit schema --format certkit/spec/v1 > spec.schema.json

Both formats have a published JSON Schema, shipped inside the wheel and validated in CI against every bundled example and 200 generated specs. SPEC.md explains the format to a person; the schema explains it to a program.

from certkit.schemas import load_schema, schema_for

load_schema("certkit/farkas/v1")  # by format id
schema_for(my_document)  # by the document's own `schema` field

Validating against them needs a JSON Schema library, which is a development dependency here — certkit itself still imports nothing outside the standard library.

certkit explain

Takes the same --spec and --cert. Prints the arithmetic and exits with the same status as check, so dropping it into a script does not launder a refusal into a success.

    [2]  payload - record_len + 19 <= 0
    [3]  -payload + record_len - 3 < 0

  Multiply each atom by its nonnegative weight and add:

    1 * [2]    (payload - record_len + 19 <= 0)
    1 * [3]    (-payload + record_len - 3 < 0)

  Every variable cancels: payload, record_len all sum to 0.

  What remains is:  16 < 0

Three verdicts, and why there are three

Verdict	Exit	Meaning
ACCEPTED	0	Every obligation was refuted and the certificate is bound to this spec.
REFUSED	1	At least one obligation was not refuted, or the input was malformed.
UNVERIFIED	3	The arithmetic checked out, but a required precondition was never established. Not a pass.

UNVERIFIED exists because of --no-fingerprint. That flag skips the check binding the certificate to the spec — useful while authoring, when the fingerprint has not been computed yet. But a certificate that was never tied to this spec has not been shown to say anything about this spec, so reporting it as accepted would be a pass on input the checker did not fully validate. It now reports UNVERIFIED and exits 3, and the reason line says TRUST ANCHOR ABSENT in those words.

In the API the same distinction is two separate booleans, because they fail separately:

report = check_certificate(spec, cert, require_fingerprint=False)
report.obligations_ok  # True  -- the multipliers really do refute the obligation
report.binding_verified  # False -- but nothing ties this certificate to this spec
report.ok  # False -- so the overall answer is no
report.verdict  # 'UNVERIFIED'

A refusal means not proven — never proven false. So does an UNVERIFIED.

The worked example

The shipped example is the CVE-2014-0160 (Heartbleed) shape. The claim is that the guard 19 + payload <= record_len implies the raw access bound 3 + payload <= record_len for every payload in [0, 65535].

from certkit import atom, make_spec, check_certificate

domain = [atom({"payload": -1}), atom({"payload": 1}, -65535)]  # 0 <= payload <= 65535
guard = [atom({"payload": 1, "record_len": -1}, 19)]  # 19 + payload <= record_len
safety = [atom({"payload": 1, "record_len": -1}, 3)]  #  3 + payload <= record_len

spec = make_spec(domain, guard, safety, name="heartbleed")

cert = {
    "schema": "certkit/farkas/v1",
    "spec_fingerprint": spec["fingerprint"],
    "obligations": [{"multipliers": {"2": 1, "3": 1}}],
}

report = check_certificate(spec, cert)
assert report  # truthy when every obligation is refuted

Those multipliers are the whole proof. Atom 2 is the guard (payload - record_len + 19 <= 0) and atom 3 is the negated safety property (-payload + record_len - 3 < 0). Add them with weight 1 each: every variable cancels and 16 < 0 remains, which is absurd — so no counterexample exists.

How it works

A Farkas certificate witnesses that a conjunction of linear atoms is unsatisfiable. It is a vector of nonnegative multipliers such that the weighted atoms sum to a contradiction: all variables cancel and the surviving constant is impossible.

Soundness in one line: if every L_i <= 0 and every m_i >= 0, then sum(m_i * L_i) <= 0 necessarily — so if the multipliers make the variables cancel and leave a positive constant, the system has no solution.

Because the integers are a subset of the rationals, rational infeasibility implies integer infeasibility. The converse does not hold, which is exactly why a failure to find a certificate is not a proof of satisfiability. This checker refuses; it does not certify the negation.

Finding the multipliers is somebody else's problem. This package contains no search. That asymmetry is what makes proof-carrying verification useful — the producer can be arbitrarily clever and entirely untrusted, because checking is cheap and auditable.

Reconstruction: why a forged certificate fails

A naive checker reads the atoms out of the certificate and verifies the multipliers against those atoms. That is close to worthless — a certificate carrying an easy, unrelated system plus a valid refutation of it would pass while proving nothing about your program.

certkit ignores any atoms a certificate carries. It rebuilds the obligation from the independently-supplied spec:

system := domain AND guard AND NOT(safety)

and lets the certificate supply only the multipliers. The certificate is additionally bound to the spec by a SHA-256 fingerprint.

That fingerprint detects drift and accidental mismatch. It is not a defence against a deliberate forger, who would simply recompute it over an edited spec. Soundness ultimately rests on a human having read the spec's relations — which are small integer inequalities, deliberately small enough to read. We would rather say that plainly than imply a guarantee the mechanism does not provide.

Sum-of-squares certificates

For nonlinear obligations target(x) >= 0, the analogous certificate is a rational identity scale * target == sum(q_i^2) with scale > 0:

certkit sos --cert my-sos-cert.json

Every square is nonnegative and the scale is positive, so the target is nonnegative. The checker re-multiplies the polynomials and verifies the identity exactly over the rationals — a perturbed certificate fails because every monomial coefficient must cancel to zero. There is no tolerance to tune.

Scope, honestly: sum-of-squares is incomplete. A nonnegative polynomial need not admit an SOS decomposition (Motzkin's polynomial is the standard witness), and nonnegativity over the integers or over a non-compact domain is a different question. A refusal means "no certificate supplied, or it did not check" — never "the target is negative".

What this package is not

• Not a solver. It never searches for a proof. Bring your own producer.
• Not a completeness oracle. Refusal is not disproof.
• Not a defence against a forger who controls the spec. See above.
• Not a whole-program verifier. It checks the obligation you hand it, over the domain you declare. Whether that obligation captures your real safety property is your judgement, and the spec is kept small so you can exercise it.

Where certificates come from

This package deliberately contains no producer. That is what keeps the trusted base small enough to read in an afternoon — and it means you need something upstream to find the multipliers.

For small problems, any LP or SMT solver will do; the format is documented in SPEC.md precisely so you can emit it from whatever you already run. Deciding obligations over full machine-word domains without enumerating them needs a solver-free elimination procedure, which is not part of this package and is available commercially.

The split is the point: the checker is free and always will be, because a certificate you cannot independently verify is worth nothing. What costs money is producing certificates at scale.

API

Function	Purpose
atom(coeff, const, strict)	build a linear atom sum(coeff*var) + const <= 0
negate(a)	logical negation; flips coefficients, constant, and strictness
verify_farkas(atoms, multipliers)	check a refutation; returns a truthy result with .reason
verify_sos(cert)	check a rational sum-of-squares identity
make_spec(domain, guard, safety, name)	build a spec with its fingerprint
check_certificate(spec, cert)	full check across every safety conjunct
reconstruct_obligation(spec)	rebuild domain AND guard AND NOT(safety)

check_certificate returns a CheckReport with .verdict, .ok, .obligations_ok, .binding_verified, .reason, and .obligations. It never raises on malformed input — a spec is attacker-controlled just like a certificate, so a zero denominator or an Infinity coefficient is a refusal carrying a reason, not a traceback.

Tests

pip install -e ".[dev]"
pytest

541 tests, and the count in this sentence is itself checked by one of them. The negative cases are the interesting ones: hostile indices, negative and float multipliers, non-cancelling variables, feasible systems, tampered specs, cross-bound certificates, and a forged certificate that carries its own easy system. A checker that accepts a valid certificate is table stakes; one that rejects near-misses is the product.

tests/test_adversarial.py is the permanent guard against one specific failure — the checker saying ACCEPTED on something it did not fully check. Its oracle is no input may produce a confident-looking answer that is wrong, and it covers malformed, empty, enormous, and out-of-distribution input, plus metamorphic relations (scaling every multiplier by any k > 0 must preserve validity; scaling by 0 must destroy it) and the CLI exit-code contract.

The rest of the toolkit

certkit	the certificate format and the independent checker
exploit-counter	if a guard is unsound, exactly how many states escape
crs-mcp	the verdict surface AI coding agents call, over MCP
soundnessbench	the benchmark that grades all of the above
certkit-action	run the check in your CI
pytest-mutation-verified	prove your regression test can actually fail
cve-proof-corpus	six real CVEs with machine-checkable proofs
Try it in your browser	no install; watch a forgery get refused

Documentation

TUTORIAL.md	a real C bounds check to a CI gate, end to end
SCOPE.md	what a verdict proves, and what it does not
TROUBLESHOOTING.md	every error string, and what fixes it
SPEC.md	the on-disk format, for emitting it from your own solver

---

The closed core

These packages are the checking half. They deliberately contain no proof search, which is what keeps them small enough to audit — and it means something upstream has to produce certificates.

For obligations over full machine-word domains, enumeration does not scale and a decision procedure that does not enumerate is required: solver-free elimination emitting replayable certificates. That engine, the repair synthesiser that derives a minimal guard from a refutation, and the evolutionary search that drives them are not in this repository and are available commercially.

The split is deliberate and permanent. The checker is free and always will be — a certificate you cannot independently verify is worth nothing, so charging for verification would defeat the format. What costs money is producing certificates at scale.

License

Apache-2.0. Copying is the point — this is a format we want adopted, not a moat.

Licence, citation, contributing

Apache-2.0 (LICENSE). If you use this in work you publish, there is machine-readable citation metadata in CITATION.cff — GitHub's "Cite this repository" button reads it.

• CONTRIBUTING.md — the house rules, and the one invariant a change must not break.
• ARCHITECTURE.md — the module map and where the trust boundary sits.
• TROUBLESHOOTING.md — keyed to the error messages this actually prints.
• SECURITY.md — a checker that accepts something false is the highest severity class here.

---

Part of certified discovery — ten artifacts built on one asymmetry: checking a proof is cheap and auditable, so the thing that produced it does not have to be trusted.