nickh007/hw-verify
hw-verify — a hardware-security verification dataset with controls Every positive example ships beside a deliberately broken counterpart, so a model or tool is graded against controls instead of against itself. Try the checker that generated this data: 🔒 hw-verify Space — paste Verilog, get a verdict, in your browser, no install. Install pip install datasets 30-second quickstart from datasets import load_dataset rtl =… See the full description on the dataset page: https://huggingface.co/datasets/nickh007/hw-verify.
hw-verify — a hardware-security verification dataset with controls
Every positive example ships beside a deliberately broken counterpart, so a model or tool is graded against controls instead of against itself.
   
Try the checker that generated this data: 🔒 hw-verify Space — paste Verilog, get a verdict, in your browser, no install.
Install
pip install datasets30-second quickstart
from datasets import load_dataset
rtl = load_dataset("nickh007/hw-verify", "rtl_constant_time", split="test")
print(rtl.num_rows, "records,", len(rtl.column_names), "fields")
scored = rtl.filter(lambda r: r["scored"])
print(scored[0]["module"], scored[0]["label"])27 records, 12 fields
barrett_ct CONSTANT_TIMEThe result that motivates the whole corpus — probes a dependence-only tool would flag:
masking = load_dataset("nickh007/hw-verify", "masking_probes", split="test")
uniformity_only = masking.filter(lambda r: r["certificate"] == "uniformity")
print(len(uniformity_only), "probes certified ONLY by uniformity")2 probes certified ONLY by uniformityWhy this exists
Security datasets in this area are almost always one-sided: a pile of vulnerable examples. A classifier that answers "vulnerable" for everything scores 100% on such a corpus, and nobody notices.
Every split here is matched. The RTL split pairs each constant-time design with a leaky twin of identical module interface. The masking split includes three gadgets that genuinely recombine a secret. The patch split includes a fix that blocks only one witness and a fix that rejects everything. If your method cannot separate the halves of a pair, its accuracy number means nothing.
Provenance
Every record is computed, not transcribed. build.py reads the actual fixture sources, runs the actual masking prover over every probe, and runs the actual solver to produce the patch certificates. Re-running it reproduces the committed files byte for byte, and a test asserts that — so the data cannot silently drift from the code that produced it.
python build.py --check # fails if the committed data is staleThe tools that generated it are open: `ctbench`, `ct-mask`, `patchproof`.
Splits
rtl_constant_time — 27 records
Verilog-2001 fixtures. 18 scored across 8 matched pairs, plus 9 unscored files kept for context (fault-detection and secret-residue designs whose observable is a data output, so grading them under a timing task would be a category error).
The out-of-remit control. barrett_buggy.v is genuinely constant-time and functionally wrong — a miscalibrated Barrett shift makes 62,206 of 65,536 coefficients disagree with the reference. A timing tool that flags it is crying wolf. It is labelled role: out_of_remit and it exists to separate serious methods from pattern-matchers.
masking_probes — 17 records
One record per probe wire of every bundled masked gadget, with the certificate that discharged it. Probe-level rather than gadget-level because the interesting datum is which certificate covered which wire.
The result that motivates the tool: two dom_and probes certify only by uniformity. They touch both shares of an operand — so a dependence-only analysis flags them — and are perfectly secure because a fresh mask always flips them.
Note that mean_invariant and distribution_invariant are recorded separately. For dom_and the mean is invariant and the distribution is not. A first-order verdict is a statement about the first moment, and the data says so rather than letting you assume more.
patch_certificates — 5 records
Modelled bounds-check defect classes, with exploit witnesses and replayable elimination certificates.
Baseline
data/baseline.json holds a reference result for the RTL split from the bundled cone-of-influence checker: 18/18 correct, 8/8 pairs separated, sound, out-of-remit control passed. It is a baseline, not a strong tool — it reasons about syntax rather than semantics and will over-report on designs where a secret reaches a completion signal by a path never taken.
Usage
from datasets import load_dataset
rtl = load_dataset("nickh007/hw-verify", "rtl_constant_time", split="test")
scored = rtl.filter(lambda r: r["scored"])
print(scored[0]["module"], scored[0]["label"])
masking = load_dataset("nickh007/hw-verify", "masking_probes", split="test")
uniformity_only = masking.filter(lambda r: r["certificate"] == "uniformity")
print(len(uniformity_only), "probes a dependence-only tool would flag")Scoring — do not use plain accuracy
The two error directions are not equally bad, and the reference implementation ranks accordingly:
pip install ctbench gives you ctbench score, ctbench validate, and ctbench leaderboard, which implement exactly this rule.
Scope and limits
- RTL labels concern completion timing against declared secrets — not power, EM, cache, or microarchitectural channels.
- Masking records are glitch-free gate-value probing, first order (d=1), 2-share.
- Patch records are reachability in modelled bit semantics — not an RCE claim. The
out_of_modelfield lists the defect shapes deliberately excluded. - Secrets are a specification choice, recorded per fixture and never inferred from source.
<!-- portfolio:start -->
Part of the hw-verify toolkit
Five open tools, a dataset, and a browser demo for proving security properties of hardware and bounds checks. They share one boundary: everything open analyses a design you disclose in full.
The commercial boundary. 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. It is not in any of these packages. <!-- portfolio:end -->
Licence
Per record, in the license field, because flattening it would misstate it. Full texts and the upstream copyright notice are in `LICENSE-DATA`:
- CC-BY-4.0 — RTL fixtures, so they can be copied into papers and slides.
- ISC —
pcpi_div.v,pcpi_mul.v,pcpi_div_wiped.v,pcpi_div_halfwipe.v, which derive from the picorv32 project by Claire Wolf and remain under the upstream licence. - Apache-2.0 — the masking and patch records, which are outputs of the tools.
Citation
@misc{hwverify2026,
title = {hw-verify: a hardware-security verification dataset with matched controls},
year = {2026},
note = {Matched-pair RTL, masking probe certificates, and patch-completeness certificates}
}Contributing
The most valuable contribution is a new matched pair for the corpus: a safe design and a leaky twin with an identical interface, so the pair cannot be won by guessing. See ctbench's CONTRIBUTING — every record here is regenerated from that corpus by build.py, so a fixture added there appears here on the next build.
The commercial boundary
Everything here concerns designs disclosed in full. Proving a property to a third party who never receives the design is a different problem — it requires the verdict bound to a commitment of a design that stays hidden — and that capability is commercial.