hw-verify-mcp
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {
"listChanged": false
} |
| experimental | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| check_constant_timeA | Decide whether a Verilog module's completion signal is independent of declared secret inputs. Returns CONSTANT_TIME or LEAKY, and on LEAKY names the secrets that reach the completion signal. You cannot declare a design constant-time yourself: re-run this tool after any fix. |
| find_leakB | Localise a timing leak: name the secret inputs that reach the completion signal, and how large its fan-in cone is. |
| list_benchmark_fixturesA | List the ctbench matched-pair corpus: constant-time designs each paired with a deliberately leaky twin of identical interface, plus an out-of-remit control. |
| get_benchmark_fixtureA | Fetch the Verilog source of one bundled benchmark fixture. |
| score_benchmark_submissionA | Grade a set of verdicts against the benchmark. Reports unsound verdicts (said safe, is leaky) separately from imprecise ones, because only the first kind ships a vulnerability. |
| run_reference_checkerB | Run the bundled cone-of-influence baseline over the whole benchmark corpus. |
| check_maskingA | Certify a masked gadget first-order secure under glitch-free probing, or name the probe wire that recombines a secret. Accepts a bundled gadget name or a JSON netlist. Two certificates are tried: dependence (touches at most one share) and uniformity (a fresh mask always flips the wire). |
| list_masking_gadgetsB | List the bundled masking gadgets and the JSON netlist format for your own. |
| check_patch_completeA | Decide whether a modelled bounds-check repair eliminates EVERY violating input, not just a known one. Returns COMPLETE, INCOMPLETE (with a surviving violating input), or VACUOUS (the guard rejects everything). |
| list_defect_classesA | List the modelled bounds-check defect classes, and what a COMPLETE verdict explicitly does not cover. |
| replay_certificateA | Re-check an elimination certificate using integer arithmetic only. No solver is used, so this verifies someone else's claim without trusting them or an SMT solver. |
| prove_confidentialB | Prove a property to a third party WITHOUT disclosing the design. Not available in the open-source distribution; call it to see what is. |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 12 tools
Most tools have clearly distinct purposes (e.g., list vs. get, check vs. replay), but check_constant_time and find_leak both analyze timing leaks, with check_constant_time already naming leaking secrets, making their boundaries slightly blurred. Descriptions mitigate confusion, but the overlap is present.
All 12 tools follow a consistent verb_noun pattern with underscores (check_*, list_*, get_*, score_*, run_*, replay_*, prove_*). No mixed conventions or camelCase appear, making the naming highly predictable.
With 12 tools spanning constant-time verification, benchmark handling, masking certification, and patch completeness, the count is well within the ideal 3-15 range. Each tool serves a distinct function, and none feel redundant or excessive.
The tool set covers the main workflows: checking constant-time, localizing leaks, running benchmarks, scoring submissions, certifying masking, and validating patches. A notable gap is prove_confidential, which is explicitly unavailable in open-source, leaving that functionality as a placeholder rather than a usable tool. Aside from this, the surface is comprehensive for the stated purpose.