Paste Verilog, get a formal verdict with the leaking signals named — not a guess.
This runs the real analyzer — the same ctbench code you can
pip install — compiled to WebAssembly and executed in your browser.
Nothing is uploaded. Nothing leaves this page.
Secrets are a specification choice and are never inferred. Naming them is
the point: a tool that guesses produces 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. It is not in any of these packages.