Artifacts & Open Source
The tools behind our methods, and the data they produce, published so anyone can use or check them. The lab code behind each result is not public yet; each result page says what you can check without it.
18open artifacts. Every link was checked when this page was built.
| Part | Name | What it is | Where |
|---|---|---|---|
| Datasets | |||
| llm-precision-fingerprints | Precision-labelled logprobs from one model at several precisions over a fixed 40-probe set, with a built-in negative control. | huggingface.co/datasets/nickh007/llm-precision-fingerprints | |
| Live demos | |||
| Wait-For Visualiser | Visualise whether a wait-for relation can wedge. | huggingface.co/spaces/nickh007/wait-for-visualiser | |
| Open-source code | |||
| isolation-tax | Measure what per-tenant KV-cache isolation costs on your own traffic. | github.com/nickharris808/isolation-tax | |
| kvprobe | Is your LLM provider serving the model you are paying for? An experimental probe for that question; its accuracy is not measured here. | github.com/nickharris808/kvprobe | |
| formal-proof-mcp | A server for AI agents (Model Context Protocol): it checks every proof step and reports any step left unproved. | github.com/nickharris808/formal-proof-mcp | |
| sf-verify | Re-derive a deployment’s admission decisions offline from a hash-chained log. | github.com/nickharris808/sf-verify | |
| proof-to-code-drift | Build checks that catch named ways a formal proof drifts from the code you ship, such as a constant changed in the code but not in the proof. | github.com/nickharris808/proof-to-code-drift | |
| tokencount | A token count both parties can recompute. | github.com/nickharris808/tokencount | |
| abstain-bench | How often a verifier claims success on input it could not check: a benchmark for unearned passes. | github.com/nickharris808/abstain-bench | |
| certhead | An experimental output head for language models that tries to certify each token and otherwise falls back to the full computation; its accuracy is not measured here. | github.com/nickharris808/certhead | |
| evidence | Runs the verification tools over your repository and gives one verdict: the weakest result, never the average. | github.com/nickharris808/evidence | |
| evidence-docs | Documentation for these verification tools. | github.com/nickharris808/evidence-docs | |
| floorgen | An experimental tool that computes a lower bound on the state a system must keep, from a description of what it must be able to recover. | github.com/nickharris808/floorgen | |
| gatecount | How many states does removing this check admit? An exact count, or a refusal when it cannot count. | github.com/nickharris808/gatecount | |
| gridlock | Checks whether a wait-for relation can deadlock, with a deliberately deadlocking example beside each case. | github.com/nickharris808/gridlock | |
| illusion-bench | Seeded kernel defects over a domain small enough to list in full: how many does your checker let through? | github.com/nickharris808/illusion-bench | |
| proof-carrying-ci | The verification tools as one CI check; the overall result is the weakest leg, never the average. | github.com/nickharris808/proof-carrying-ci | |
| signoff-cert | A certificate format whose false-pass bound and scope are required, machine-readable fields. | github.com/nickharris808/signoff-cert | |
Read from the Hugging Face and GitHub interfaces when this page was built.
How the numbers on this page are checked
Every number on this page links to the file it comes from. All published files.
- Loadingshown only once its file has loaded in your browser
- Not checkeda question we have not checked would say so, with no number
- Checked, nothing founda search that found nothing would say so, with no number
- No valuea file that holds no value for the question would say so
- File missinga number whose file is missing or altered would be hidden
- Unclear subjecttwo files that disagree about what a number describes would both be shown
- Small samplea number from a small sample would carry its sample size
- Conflicting filestwo files giving different values would both be shown
- Not publishablea file we may not publish would be named by its fingerprint only
- Out of datea measurement older than a week would carry its age
- Does not applya question that does not apply to this page would say so
- Run faileda measurement whose program failed would say so, with no number