---
title: certkit — check the proof, not the promise
emoji: 🔏
colorFrom: green
colorTo: blue
sdk: static
app_file: index.html
pinned: false
license: apache-2.0
tags:
  - formal-verification
  - security
  - proof-carrying-code
short_description: Verify safety proofs in-browser. Watch a forgery be refused.
---

# certkit — check the proof, not the promise

**You should not have to trust the tool that produced a proof in order to believe the proof.**

This Space runs the whole checker **in your browser**. The Python is executed by Pyodide under
WebAssembly, with exact rational arithmetic throughout — no solver, no floating point on the verdict
path, and **nothing you type is sent anywhere**.

That is not a compromise, it is the point: a verifier you have to trust a server to run is a weaker
object than one you can watch execute locally.

## What this page is, and what it is not

Being precise about this, because the difference is the whole argument:

- **It fetches a runtime.** On first load the page downloads the pinned Pyodide 0.27.3 runtime from
  `cdn.jsdelivr.net` — that is the few seconds you wait. After that it makes no further requests, and
  no certificate you paste ever leaves your machine. "Nothing is uploaded" is true; "this page makes
  no network requests at all" is **not**, and other pages in this portfolio should not be read as
  making that promise on this one's behalf.
- **It is not the zero-download verifier.** There is a second, separate artifact — a plain-JavaScript
  checker that runs with no runtime download at all and answers `ACCEPT`, `REJECT` or `REFUSE`, where
  `REFUSE` means it declined to judge a document it does not understand rather than calling it
  invalid. That one is measured against a corpus with both degenerate strategies (accept-everything
  and reject-everything) scored beside it, and it is not published yet. This page and that one check
  the same certificates and are not the same object.
- **What is measured here.** `tests/test_render.py` opens this page in a real browser and fails if a
  visitor would see anything but a verdict. That is a rendering guarantee, not a soundness one; the
  soundness argument is in `certkit` itself, which this page inlines.


## 30-second quickstart

Nothing to install — the checker runs in this page under Pyodide.

1. The page opens on **Check a certificate** with a real pair already checked → `ACCEPTED`.
2. Press **Load a forgery** → `REFUSED`, with the arithmetic that failed:
   `non-strict combination needs const > 0, got -65535`.
3. Open **Six real CVEs** and press **Re-check all 6 now** → `6 of 6 re-checked successfully`.

Nothing you type is uploaded. There is no server: the page carries the real checker, and your
browser runs it.

Want the same thing locally?

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

## Three things to try

**1. Certify a guard.** Set a bounds check and the safety property it is supposed to imply. If the
check is too weak you get the exact number of escaping inputs and a concrete counterexample:

```
## PROVEN UNSOUND
The guard admits 509 states the safety property forbids, out of 65,536.

Counterexample: payload = 0, record_len = 1
At that input the guard passes (1 + 0 <= 1) but the safety property does not hold.

Per-draw hit probability: 0.00777
Expected uniform draws to find one: 129
```

That last line is the point: a fuzzer needs ~129 random draws to stumble on it, and rarer gaps take
billions.

**2. Check a certificate — then load a forgery.** The forgery carries a valid refutation of its
*own* easier system. It still fails, because the checker rebuilds the obligation from the spec and
ignores whatever atoms the certificate brought with it.

**3. Re-check six real CVEs.** Heartbleed (CVE-2014-0160), Baron Samedit (CVE-2021-3156), the zlib
inflate overflow (CVE-2022-37434), and three more — with their real upstream relations and real
Farkas multipliers. Press the button and all six are re-verified live in your session.

## What a proof looks like here

A guard is proven sound by exhibiting nonnegative multipliers that combine the guard with the
*negated* safety property so that every variable cancels and an impossible constant remains.

For Heartbleed the entire proof is `{"2": 1, "3": 1}`. Atom 2 is the guard
(`payload - record_len + 19 <= 0`), atom 3 is the negated safety property
(`-payload + record_len - 3 < 0`). Add them: everything cancels and `16 < 0` remains, which is
absurd. So no counterexample exists.

Checking that is arithmetic. Finding it is the hard part — and this package deliberately contains no
search, which is what keeps the trusted base small enough to read in an afternoon.

## Scope, stated plainly

The verdict comes from exhaustive integer counting over the domain you declare. That is sound and
complete **for that domain** and silent outside it.

The demo caps the domain at 4,095 so it answers instantly. That is a limit of the *demo*, not of the
method. Deciding full 32-bit domains needs a decision procedure that does not enumerate — solver-free
elimination emitting replayable certificates — which is not part of the open packages and is
available commercially.

## How this Space is built

`index.html` is generated by `build_static.py`, which inlines the real `certkit` and
`exploit-counter` sources and mounts them into a **pinned** Pyodide runtime. The published Space
therefore cannot drift from the packages it claims to run — regenerate with:

```bash
python build_static.py
```

No *package* is installed at page load. There is no `micropip`, no package index, and no dependency
resolution on the boot path: everything mounted is standard-library-only, which is the same property
the packages themselves advertise. The Pyodide runtime itself is fetched from the CDN pinned above,
which is the one network request this page makes. An earlier build did resolve `gradio` and its transitive
dependencies from live PyPI on every visit, and broke when one of those pins stopped being
satisfiable — a page that needed a package index to render was quietly contradicting the thing it
was demonstrating. `tests/test_render.py` opens this page in a real browser and fails if a visitor
would see anything other than a verdict.

## Run it yourself

```bash
pip install "certkit@git+https://github.com/nickharris808/certkit@main" \
            "exploit-counter@git+https://github.com/nickharris808/exploit-counter@main"
certkit demo
```

- [`certkit`](https://github.com/nickharris808/certkit) — the format and the checker
- [`exploit-counter`](https://github.com/nickharris808/exploit-counter) — the counting engine
- `cve-proof-corpus` — the six CVE records this Space verifies

## The rest of the toolkit

| | |
|---|---|
| **[certkit](https://github.com/nickharris808/certkit)** | the checker running in this page |
| **[exploit-counter](https://github.com/nickharris808/exploit-counter)** | the counting engine behind the escape counts |
| **[cve-proof-corpus](https://huggingface.co/datasets/nickh007/cve-proof-corpus)** | the six CVE records verified in tab 3 |
| **[soundnessbench](https://github.com/nickharris808/soundnessbench)** | the benchmark that grades soundness tools |
| **[crs-mcp](https://github.com/nickharris808/crs-mcp)** | give your AI coding agent the same verdicts |

## License

Apache-2.0.

---

Part of **[certified discovery](https://nickharris808.github.io/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.