One bounds check, end to end

Fifteen minutes, four tools, and a real vulnerability shape. Every command below was run to produce the output shown; if you paste them in order you get the same thing, because none of the numbers on this page were typed by hand.

Setup

python -m venv venv && source venv/bin/activate
pip install "certkit@git+https://github.com/nickharris808/certkit@main" \
            "exploit-counter@git+https://github.com/nickharris808/exploit-counter@main"

Neither package has a runtime dependency. The install is fetching source, not a dependency tree.

1. The check you are trying to justify

This is the Heartbleed shape, in C:

/* attacker controls payload; record_len is the real record size */
if (19 + payload <= record_len) {
    memcpy(dst, src + 3, payload);   /* needs 3 + payload <= record_len */
}

The guard is 19 + payload <= record_len. The property the memcpy needs is 3 + payload <= record_len. The claim is that the first implies the second, for every attacker-controlled payload in range.

2. Write the specification

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

You never hand-write JSON atoms. certkit init rejects == (that is two relations — write both), chained comparisons, and anything nonlinear, rather than guessing what you meant.

3. Ask whether the guard is sound at all

Before proving anything, find out whether there is anything to prove. This enumerates the declared box exactly:

exploit-counter check --spec heartbleed.spec.json --box "payload=0..255,record_len=0..255"

A sound guard reports zero escaping states. Try it with the guard weakened to 1 + payload <= record_len and you get a count and a concrete counterexample — payload = 0, record_len = 1 passes that guard and violates safety. That is the fastest way to discover you are about to try proving something false.

4. Prove it

certkit ships no producer, so the multipliers come from you or from a solver. For this obligation they are one line: weight 1 on the guard, weight 1 on the negated safety conjunct. Write heartbleed.cert.json:

{
  "schema": "certkit/farkas/v1",
  "spec_fingerprint": "<paste the fingerprint from the spec>",
  "obligations": [{ "multipliers": { "2": 1, "3": 1 } }]
}

Indices are positions in the rebuilt obligation: domain atoms first, then guard, then the negated safety conjunct.

certkit check --spec heartbleed.spec.json --cert heartbleed.cert.json

ACCEPTED
  obligation 0: ok

To see the arithmetic rather than the verdict:

certkit explain --spec heartbleed.spec.json --cert heartbleed.cert.json

5. Watch it refuse a forgery

Change any multiplier and check again. The refusal names what failed — non-strict combination needs const > 0, got -65535 — rather than saying "invalid". Change the guard constant in the spec without recomputing the fingerprint and you get a different refusal: certificate is bound to a different spec.

6. Have a solver check the same claim

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

unsat is the same claim ACCEPTED makes, reached by an implementation that shares no code with certkit. If a solver ever said sat where certkit said ACCEPTED, one of them would be unsound — which is why that comparison runs in CI on every push rather than living in a paragraph like this one.

7. Put it in the gate

GitHub Actions:

- uses: nickharris808/certkit-action@main
  with:
    spec: heartbleed.spec.json
    cert: heartbleed.cert.json

Locally, on every commit:

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

Both treat exit 3 — UNVERIFIED, the tool declining to certify — as a failure. In a gate, "declined to certify" and "refused" have the same consequence. Both also fail when a certificate has no spec beside it, rather than skipping: a gate that silently skips what it cannot check will happily report that all certificates verified while verifying none.

GitLab and CircleCI templates are in certkit/ci-templates/.

8. While you type

certkit lsp

Point an editor's LSP client at that for *.spec.json and the diagnostics arrive while you are still thinking about the guard, instead of after CI stops you merging. It reports structural problems, the verdict of a certificate sitting beside the spec, and variables the domain never bounds. It never offers to fix a guard, and it never tells you one is correct.

What you have, and what you do not

You have a machine-checkable proof that these relations imply each other, re-checkable by anyone in seconds, in Python or in JavaScript, with no solver and no trust in whatever produced it. You do not have a proof that your C is safe — that depends on whether the spec models the code, and on whether the arithmetic in it can wrap. What this proves, and what it does not is the page about that.