Open tools that prove security properties of hardware — and refuse rather than guess.
Constant-time RTL, masking gadgets, and bounds-check patches. Three checkers, one discipline: a verdict is earned or it is not given.
▶ Try it in your browser Install The tools
Every tool here answers one question in a different domain:
Does a secret reach something an attacker can observe?
For RTL that observable is completion timing. For a masking gadget it is a probed wire. For a bounds check it is whether any violating input still gets through. Same shape, three domains — which is why these are one body of work rather than three coincidences.
Most analysis tools have two answers. These have three, and the third is the one that matters:
| Verdict | Meaning | Exit |
|---|---|---|
| CONSTANT_TIME | No declared secret reaches the observable, within the analysable subset. | 0 |
| LEAKY | One does — and the reaching signals are named, so you can check. | 1 |
| UNKNOWN | No verdict. The analysis could not read the design and says so. | 2 |
A checker that skips what it cannot parse does not become vaguer — it deletes dependency edges, and a signal with no edges has an empty cone, and an empty cone contains no secrets, and no secrets reads as safe. That is a confident wrong answer in the dangerous direction, and it is the specific failure everything here is built to prevent.
UNKNOWN exits 2 rather than 1 so a CI job
guarding only against "leaky" cannot be satisfied by "we could not tell".
pip install git+https://github.com/nickharris808/hw-verify@main
hw-verify ct check rtl/*.v --secret key # timing leaks in RTL
hw-verify ct explain rtl/cmp.v --secret key # ...and HOW the secret reaches it
hw-verify mask check dom_and # a masked gadget, probe by probe
hw-verify patch check # bounds-check patches, proved completeA leak is not just flagged, it is traced:
$ hw-verify ct explain cmp_leaky.v
LEAKY — 'done' depends on x, y.
How each secret reaches it (shortest path first):
x
├─ xr
└─ doneThat matters because the analysis over-approximates: it follows every dependency edge whether or not the path can be taken at run time. Without the path you cannot tell a real finding from a dead one, and you learn to distrust the tool. With it you read four signal names and decide.
Constant-time RTL. A matched-pair benchmark — every safe design ships beside a leaky twin with an identical interface — plus a leaderboard that ranks soundness first. Reads Verilog, or a synthesised Yosys netlist for hierarchical designs.
First-order masking, by two certificates. Adds a uniformity certificate that certifies gadgets a dependence-only tool reports as leaky — and is honest that a first-order verdict is a statement about the first moment only.
Does your bounds-check fix eliminate every violating input, or just the one you found? Emits a Farkas certificate a third party replays with integer arithmetic — no solver required.
That certificate, re-checked in Rust, sharing no code with the prover. Both implementations run the same 30 test vectors and a disagreement fails both builds. This is what makes "verify without trusting us" a property.
The RTL check on every pull request, as diff annotations and a job summary. Files that reach no verdict are counted separately and never rendered as a pass.
All three checkers as MCP tools, so an AI agent writing RTL gets a checker it
cannot argue with. Every refusal carries a next_step, and the agent
cannot set the verdict itself.
| hw-verify | Verdicts: RTL fixtures, masking probes, patch certificates. What each design is. |
| hw-verify-paths | Dependency graphs and witness paths. Why — reasoning traces, not labels. |
Each tool ships a SCOPE.md stating its limits precisely. In summary:
verdicts cover the modelled channel only — not power, EM, cache, or
microarchitectural leakage. Secrets are a specification choice and are
never inferred: guessing which inputs are sensitive would produce confident
verdicts about the wrong property.
The commercial boundary. Everything here analyses a design you disclose in full. Proving a property to a third party who never receives the design — a verdict bound to a commitment of a design that stays hidden — is a different problem, and a commercial one. Nothing in these packages implements it.
| Live demo | Paste Verilog, get a verdict. No install, nothing uploaded. |
| Tutorial | Find a leak, fix it, put the check in CI. Ten minutes. |
| Honest scope | What a verdict proves, and the constructs the analysis refuses. |
| FAQ | The objections people actually raise. |
| Install | One package, three checkers. |