README.md

metadata

title: Wait-For Visualiser
emoji: 🔗
colorFrom: indigo
colorTo: gray
sdk: static
app_file: index.html
pinned: false
license: apache-2.0
tags:
  - deadlock
  - verification
  - formal-methods
  - distributed-systems
  - visualisation

Will it wedge? Paste a wait-for graph and find out

Paste a {waiter: [waited-on]} mapping and this exhibits the cycle if one exists — the exact argument gridlock makes, running entirely in your browser. Nothing is uploaded.

It abstains on an empty graph. A graph with no nodes has no cycle, so "no deadlock" is true and tells you nothing about your system — and the overwhelmingly likely cause of an empty graph is a config that failed to load. Reporting SAFE there would be a confident answer nobody earned.

Run the same check locally, including importers that build the graph from Kubernetes manifests or Python source:

pip install gridlock
gridlock import k8s ./manifests | gridlock check -

The page reimplements gridlock's decision procedure in JavaScript, and a reimplementation is a second chance to be wrong. differential_test.py in this Space checks the two against each other on random graphs: 400 graphs, gridlock found a cycle in 343, 0 disagreements. Re-run it yourself with python3 differential_test.py (needs node and pip install gridlock).

---

The rest of the portfolio

25 artifacts, one idea: a measurement you cannot check is a press release. Every tool here reports; none of them gates.

Tools

abstain-bench	how often does a verifier pass input it could not check?
evidence	run the whole portfolio over your repo — the weakest leg, never the mean
floorgen	what must your system remember? an exact lower bound
formal-proof-mcp	a proof kernel for your coding agent
gatecount	exactly how many states does removing this check admit?
gridlock	certify a wait-for relation cannot wedge
honestbench	measure your CI's escape rate
kvleak	cross-tenant leak scanner
kvprobe	model-substitution detector with a measured FPR
preregister	refuses to seal a plan whose conclusion is already fixed
proof-carrying-ci	the whole portfolio as one CI check, with SARIF
proof-to-code-drift	fail the build when the proof stops matching
sf-verify	re-derive admission decisions offline
signoff-cert	certificates that carry their own false-pass bound
tokencount	a token count both parties can recompute

Benchmarks — each recomputes one of our own published numbers from its certificate

illusion-bench	how many broken kernels does your oracle admit?
kv-reuse-econ-bench	recompute our economics headline
llm-tenant-isolation-bench	recompute our isolation figures

Datasets

abstain-corpus	32 inputs a verifier must NOT pass
kv-reuse-econ-traces	per-workload reuse accounting + the closed form
kv-tenant-isolation-bench	isolation observations, uninterpretable rows included
llm-precision-fingerprints	precision-labelled logprobs with a negative control

Try it in a browser — no install, no GPU

negative-results-atlas	ten claims we took back
tenant-leak-demo	the residency calculator
wait-for-visualiser	paste a wait-for graph, see the cycle ← you are here

Documentation

Everything above, explained in one place: https://nickharris808.github.io/evidence-docs/ — the tutorial, what this proves and what it does not, and a CLI reference generated by running --help on every published command.

The commercial edition

Everything above is measure-only and Apache-2.0: it tells you what is true and never acts on it. The enforcement side — binding a partition key at the admission decision, the compiled gate corpus, and the certificate-issuing faucet — is covered by filed patents and licensed separately.

Reading is free. Enforcing is licensed.