--- 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`](https://github.com/nickharris808/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: ```bash 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`](https://github.com/nickharris808/abstain-bench) | how often does a verifier pass input it could not check? | | [`evidence`](https://github.com/nickharris808/evidence) | run the whole portfolio over your repo — the weakest leg, never the mean | | [`floorgen`](https://github.com/nickharris808/floorgen) | what must your system remember? an exact lower bound | | [`formal-proof-mcp`](https://github.com/nickharris808/formal-proof-mcp) | a proof kernel for your coding agent | | [`gatecount`](https://github.com/nickharris808/gatecount) | exactly how many states does removing this check admit? | | [`gridlock`](https://github.com/nickharris808/gridlock) | certify a wait-for relation cannot wedge | | [`honestbench`](https://github.com/nickharris808/honestbench) | measure your CI's escape rate | | [`kvleak`](https://github.com/nickharris808/kvleak) | cross-tenant leak scanner | | [`kvprobe`](https://github.com/nickharris808/kvprobe) | model-substitution detector with a measured FPR | | [`preregister`](https://github.com/nickharris808/preregister) | refuses to seal a plan whose conclusion is already fixed | | [`proof-carrying-ci`](https://github.com/nickharris808/proof-carrying-ci) | the whole portfolio as one CI check, with SARIF | | [`proof-to-code-drift`](https://github.com/nickharris808/proof-to-code-drift) | fail the build when the proof stops matching | | [`sf-verify`](https://github.com/nickharris808/sf-verify) | re-derive admission decisions offline | | [`signoff-cert`](https://github.com/nickharris808/signoff-cert) | certificates that carry their own false-pass bound | | [`tokencount`](https://github.com/nickharris808/tokencount) | a token count both parties can recompute | **Benchmarks** — each recomputes one of our own published numbers from its certificate | | | |---|---| | [`illusion-bench`](https://github.com/nickharris808/illusion-bench) | how many broken kernels does your oracle admit? | | [`kv-reuse-econ-bench`](https://github.com/nickharris808/kv-reuse-econ-bench) | recompute our economics headline | | [`llm-tenant-isolation-bench`](https://github.com/nickharris808/llm-tenant-isolation-bench) | recompute our isolation figures | **Datasets** | | | |---|---| | [`abstain-corpus`](https://huggingface.co/datasets/nickh007/abstain-corpus) | 32 inputs a verifier must NOT pass | | [`kv-reuse-econ-traces`](https://huggingface.co/datasets/nickh007/kv-reuse-econ-traces) | per-workload reuse accounting + the closed form | | [`kv-tenant-isolation-bench`](https://huggingface.co/datasets/nickh007/kv-tenant-isolation-bench) | isolation observations, uninterpretable rows included | | [`llm-precision-fingerprints`](https://huggingface.co/datasets/nickh007/llm-precision-fingerprints) | precision-labelled logprobs with a negative control | **Try it in a browser** — no install, no GPU | | | |---|---| | [`negative-results-atlas`](https://huggingface.co/spaces/nickh007/negative-results-atlas) | ten claims we took back | | [`tenant-leak-demo`](https://huggingface.co/spaces/nickh007/tenant-leak-demo) | the residency calculator | | [`wait-for-visualiser`](https://huggingface.co/spaces/nickh007/wait-for-visualiser) | paste a wait-for graph, see the cycle ← you are here | ### Documentation Everything above, explained in one place: **** — the [tutorial](https://nickharris808.github.io/evidence-docs/start/tutorial/), [what this proves and what it does not](https://nickharris808.github.io/evidence-docs/concepts/what-this-proves/), and a [CLI reference](https://nickharris808.github.io/evidence-docs/reference/cli/) 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.**