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.

Localise a timing leak: name the secret inputs that reach the completion signal, and how large its fan-in cone is.

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.

Fetch the Verilog source of one bundled benchmark fixture.

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 the bundled cone-of-influence baseline over the whole benchmark corpus.

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 the bundled masking gadgets and the JSON netlist format for your own.

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 the modelled bounds-check defect classes, and what a COMPLETE verdict explicitly does not cover.

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 a property to a third party WITHOUT disclosing the design. Not available in the open-source distribution; call it to see what is.