CLI reference¶
Generated by running --help on every published console script. If a command below does not exist, this build is broken — there is no hand-written copy of any of it.
Every command follows the same exit-code contract: 0 checked and holds · 1 checked and fails · 2 NOT checked. See Verdicts.
abstain-bench¶
$ abstain-bench --help
usage: abstain-bench [-h] [--version] {corpus,export,score,selftest} ...
how often does a verifier claim success on input it cannot check? (measure-
only)
positional arguments:
{corpus,export,score,selftest}
corpus what the corpus contains and why each case counts
export write every case to disk
score run a subject over the corpus
selftest run the benchmark against itself
options:
-h, --help show this help message and exit
--version show program's version number and exit
abstain-bench corpus¶
$ abstain-bench corpus --help
usage: abstain-bench corpus [-h]
options:
-h, --help show this help message and exit
abstain-bench export¶
$ abstain-bench export --help
usage: abstain-bench export [-h] out
positional arguments:
out
options:
-h, --help show this help message and exit
abstain-bench score¶
$ abstain-bench score --help
usage: abstain-bench score [-h] --subject SUBJECT [--name NAME]
[--timeout TIMEOUT] [--json]
options:
-h, --help show this help message and exit
--subject SUBJECT shell command; `{input}` is replaced with the case path,
or the path is appended if the placeholder is absent
--name NAME label for the report
--timeout TIMEOUT
--json
abstain-bench selftest¶
$ abstain-bench selftest --help
usage: abstain-bench selftest [-h] [--timeout TIMEOUT]
options:
-h, --help show this help message and exit
--timeout TIMEOUT
evidence¶
$ evidence --help
usage: evidence [-h] [--version] {audit,tools} ...
run the portfolio over your repository and emit ONE aggregate verdict
(measure-only)
positional arguments:
{audit,tools}
audit detect what applies, run it, aggregate to the weakest leg
tools what can run here, and what deliberately cannot
options:
-h, --help show this help message and exit
--version show program's version number and exit
evidence audit¶
$ evidence audit --help
usage: evidence audit [-h] [--format {json,junit,markdown,sarif,text}]
[--json] [--only NAME[,NAME...]] [--timeout TIMEOUT]
[--show-excluded]
[path]
positional arguments:
path
options:
-h, --help show this help message and exit
--format {json,junit,markdown,sarif,text}
--json shorthand for --format json
--only NAME[,NAME...]
restrict to these constituents
--timeout TIMEOUT per-constituent seconds
--show-excluded also list the tools that are deliberately not auto-run
evidence tools¶
$ evidence tools --help
usage: evidence tools [-h]
options:
-h, --help show this help message and exit
floorgen¶
$ floorgen --help
usage: floorgen [-h] {floor,impossible,recoveries,selftest} ...
Describe what your system must be able to recover; get the state floor.
positional arguments:
{floor,impossible,recoveries,selftest}
floor compute the exact state floor for a spec
impossible prove a budget cannot meet a spec
recoveries the worked recoveries and their floors
selftest check every floor against a hand-computed value
options:
-h, --help show this help message and exit
floorgen floor¶
$ floorgen floor --help
usage: floorgen floor [-h] [-b] [--budget-states BUDGET_STATES]
[--budget-bits BUDGET_BITS] [--json]
spec
positional arguments:
spec
options:
-h, --help show this help message and exit
-b, --builtin `spec` names a worked recovery
--budget-states BUDGET_STATES
also test a state budget for impossibility
--budget-bits BUDGET_BITS
also test a bit budget for impossibility
--json
floorgen impossible¶
$ floorgen impossible --help
usage: floorgen impossible [-h] [-b] [--budget-states BUDGET_STATES]
[--budget-bits BUDGET_BITS] [--json]
spec
positional arguments:
spec
options:
-h, --help show this help message and exit
-b, --builtin
--budget-states BUDGET_STATES
--budget-bits BUDGET_BITS
--json
floorgen recoveries¶
$ floorgen recoveries --help
usage: floorgen recoveries [-h]
options:
-h, --help show this help message and exit
floorgen selftest¶
$ floorgen selftest --help
usage: floorgen selftest [-h]
options:
-h, --help show this help message and exit
formal-proof-mcp¶
$ formal-proof-mcp --help
formal_proof_mcp.server — a Model Context Protocol server over stdio, dependency-free.
WHY NO SDK. An MCP server is a JSON-RPC 2.0 loop over stdin/stdout. Implementing it directly keeps
this package installable with zero dependencies and keeps the whole transport auditable in one
short file — which matters for a tool whose entire purpose is that an agent can trust its answers.
WHAT AN AGENT GETS. Six tools, and one invariant that runs through all of them:
a result that was not checked is never returned as a result that passed.
Every response carries `status` ∈ {ok, failed, unavailable}, and `unavailable` is kept distinct
from both. An agent that reads "no Lean toolchain installed" as "no errors found" will assert a
proof it never checked — so this server makes that specific confusion impossible to express.
Run it: `formal-proof-mcp` (stdio; wire it into Claude Desktop or Cursor)
Try it: `formal-proof-mcp --selftest`
--selftest prove each tool fires
--list-tools the 10 tools this server exposes
--version
With no flags: serve MCP over stdio.
gatecount¶
$ gatecount --help
usage: gatecount [-h] [--sample SAMPLE] [--seed SEED] [--json]
{count,removing,compare,selftest} ...
Replace 'we found zero escapes' with an exact count of what a check keeps out.
positional arguments:
{count,removing,compare,selftest}
count how many states does a policy admit?
removing how many extra states does the weakened policy admit?
compare both directions of the difference between two policies
selftest counts checked against hand-computed values
options:
-h, --help show this help message and exit
--sample SAMPLE sample this many points instead of enumerating; the
result is marked APPROXIMATE and carries an exact
binomial interval
--seed SEED
--json
gatecount count¶
$ gatecount count --help
usage: gatecount count [-h] domain policy
positional arguments:
domain
policy
options:
-h, --help show this help message and exit
gatecount removing¶
$ gatecount removing --help
usage: gatecount removing [-h] domain policy weakened
positional arguments:
domain
policy
weakened
options:
-h, --help show this help message and exit
gatecount compare¶
$ gatecount compare --help
usage: gatecount compare [-h] domain a b
positional arguments:
domain
a
b
options:
-h, --help show this help message and exit
gatecount selftest¶
$ gatecount selftest --help
usage: gatecount selftest [-h]
options:
-h, --help show this help message and exit
gridlock¶
$ gridlock --help
usage: gridlock [-h] [--version] {check,import,demo,domains} ...
certify that a wait-for relation cannot wedge (measure-only)
positional arguments:
{check,import,demo,domains}
check certify a wait-for graph from JSON
import build a wait-for graph from a real source (pipe into
`gridlock check -`)
demo certify a built-in domain and its foil
domains list the built-in domains
options:
-h, --help show this help message and exit
--version show program's version number and exit
gridlock check¶
$ gridlock check --help
usage: gridlock check [-h] [--json] file
positional arguments:
file path to the JSON graph, or "-" to read it from stdin
options:
-h, --help show this help message and exit
--json
gridlock import¶
$ gridlock import --help
usage: gridlock import [-h] [--json] {k8s,python} path
Build a wait-for graph from artefacts you already have. An importer that
cannot see anything ABSTAINS and writes no graph, so a refusal can never be
piped into `check` and become a SAFE certificate.
positional arguments:
{k8s,python} k8s: Kubernetes manifests: workload waits on workload it
reaches via a Service; python: Python source: lock A waits on
lock B when B is taken while A is held
path file or directory to read
options:
-h, --help show this help message and exit
--json full import result (verdict, scope notes, graph) instead of
the bare graph
gridlock demo¶
$ gridlock demo --help
usage: gridlock demo [-h]
[{agent-tools,kubernetes,noc,pipeline,routing-policy,vehicles,warehouse}]
positional arguments:
{agent-tools,kubernetes,noc,pipeline,routing-policy,vehicles,warehouse}
options:
-h, --help show this help message and exit
gridlock domains¶
$ gridlock domains --help
usage: gridlock domains [-h]
options:
-h, --help show this help message and exit
honestbench¶
$ honestbench --help
usage: honestbench [-h] [--version]
{manifest,verify,bound,absence,mutation,selftest} ...
evidence-honesty primitives (measure-only)
positional arguments:
{manifest,verify,bound,absence,mutation,selftest}
manifest build a sha256 manifest over a directory
verify re-hash a directory against a manifest
bound exact binomial bound for a k-of-n record
absence DELETE each evidence file; report who noticed
mutation CORRUPT each artifact; report who noticed
selftest run the package's own positive controls
options:
-h, --help show this help message and exit
--version show program's version number and exit
honestbench manifest¶
$ honestbench manifest --help
usage: honestbench manifest [-h] [--out OUT] directory
positional arguments:
directory
options:
-h, --help show this help message and exit
--out OUT
honestbench verify¶
$ honestbench verify --help
usage: honestbench verify [-h] manifest directory
positional arguments:
manifest
directory
options:
-h, --help show this help message and exit
honestbench bound¶
$ honestbench bound --help
usage: honestbench bound [-h] -n N [-k K] [--conf CONF]
options:
-h, --help show this help message and exit
-n N trials
-k K observed failures (default 0)
--conf CONF
honestbench absence¶
$ honestbench absence --help
usage: honestbench absence [-h] --spec SPEC [--json]
options:
-h, --help show this help message and exit
--spec SPEC JSON spec (see the module docstring)
--json
honestbench mutation¶
$ honestbench mutation --help
usage: honestbench mutation [-h] --spec SPEC [--json]
options:
-h, --help show this help message and exit
--spec SPEC JSON spec (see the module docstring)
--json
honestbench selftest¶
$ honestbench selftest --help
usage: honestbench selftest [-h]
options:
-h, --help show this help message and exit
kvleak¶
$ kvleak --help
usage: kvleak [-h] [--version] {residency,plan,scan,selftest} ...
does your serving stack leak between tenants? (measure-only)
positional arguments:
{residency,plan,scan,selftest}
residency can a null from this probe set even be interpreted?
plan what probe set IS interpretable on this model and
budget
scan live cross-tenant probe (needs an endpoint)
selftest positive controls for the tool itself
options:
-h, --help show this help message and exit
--version show program's version number and exit
kvleak residency¶
$ kvleak residency --help
usage: kvleak residency [-h] [--model MODEL] [--config CONFIG] --kv-budget-gib
KV_BUDGET_GIB [--prefixes PREFIXES] [--tokens TOKENS]
[--safety-margin SAFETY_MARGIN] [--json]
options:
-h, --help show this help message and exit
--model MODEL a known name, or a label for --config
--config CONFIG path to a HuggingFace config.json
--kv-budget-gib KV_BUDGET_GIB
GiB of KV cache the engine actually has (after
weights)
--prefixes PREFIXES
--tokens TOKENS
--safety-margin SAFETY_MARGIN
--json
kvleak plan¶
$ kvleak plan --help
usage: kvleak plan [-h] [--model MODEL] [--config CONFIG] --kv-budget-gib
KV_BUDGET_GIB
options:
-h, --help show this help message and exit
--model MODEL a known name, or a label for --config
--config CONFIG path to a HuggingFace config.json
--kv-budget-gib KV_BUDGET_GIB
GiB of KV cache the engine actually has (after
weights)
kvleak scan¶
$ kvleak scan --help
usage: kvleak scan [-h] [--engine {vllm,sglang}] [--base-url BASE_URL]
[--include-unfixed]
options:
-h, --help show this help message and exit
--engine {vllm,sglang}
--base-url BASE_URL
--include-unfixed enable probe 4, which automates an UNFIXED upstream
defect
kvleak selftest¶
$ kvleak selftest --help
usage: kvleak selftest [-h]
options:
-h, --help show this help message and exit
preregister¶
$ preregister --help
usage: preregister [-h] {check,seal,verify,score,selftest} ...
Seal an experiment plan — and refuse to seal one whose conclusion is already
fixed.
positional arguments:
{check,seal,verify,score,selftest}
check analyse a spec's decision rule without sealing it
seal analyse, then bind the plan to a digest and a commit
verify recompute a seal's digest
score apply a sealed rule to observed results
selftest point the tool at its own scar
options:
-h, --help show this help message and exit
preregister check¶
$ preregister check --help
usage: preregister check [-h] [--json] spec
positional arguments:
spec
options:
-h, --help show this help message and exit
--json
preregister seal¶
$ preregister seal --help
usage: preregister seal [-h] [-o OUT] [--repo REPO] [--timestamp TIMESTAMP]
[--allow-unfalsifiable]
spec
positional arguments:
spec
options:
-h, --help show this help message and exit
-o OUT, --out OUT write the sealed record here
--repo REPO repository to read the commit from
--timestamp TIMESTAMP
override the seal timestamp (for reproducible tests)
--allow-unfalsifiable
seal anyway, and STAMP the record with the reason it
should not have been sealed
preregister verify¶
$ preregister verify --help
usage: preregister verify [-h] seal
positional arguments:
seal
options:
-h, --help show this help message and exit
preregister score¶
$ preregister score --help
usage: preregister score [-h] [-r RESULTS] [--set NAME=VALUE] [--json] seal
positional arguments:
seal
options:
-h, --help show this help message and exit
-r RESULTS, --results RESULTS
JSON object of observed metric values
--set NAME=VALUE
--json
preregister selftest¶
$ preregister selftest --help
usage: preregister selftest [-h]
options:
-h, --help show this help message and exit
proof-carrying-ci¶
$ proof-carrying-ci --help
usage: proof-carrying-ci [-h] {run,explain,selftest} ...
Run the verification portfolio over your repo. The aggregate is the weakest
leg, never the mean.
positional arguments:
{run,explain,selftest}
run audit a directory
explain why fail-on defaults the way it does
selftest the aggregation rule, checked
options:
-h, --help show this help message and exit
proof-carrying-ci run¶
$ proof-carrying-ci run --help
usage: proof-carrying-ci run [-h] [--path PATH]
[--fail-on {failure,unverified,never}]
[--sarif SARIF] [--summary SUMMARY] [--json]
options:
-h, --help show this help message and exit
--path PATH
--fail-on {failure,unverified,never}
--sarif SARIF write SARIF here
--summary SUMMARY
--json
proof-carrying-ci explain¶
$ proof-carrying-ci explain --help
usage: proof-carrying-ci explain [-h]
options:
-h, --help show this help message and exit
proof-carrying-ci selftest¶
$ proof-carrying-ci selftest --help
usage: proof-carrying-ci selftest [-h]
options:
-h, --help show this help message and exit
proof-drift¶
$ proof-drift --help
usage: proof-drift [-h] [--version] {check,source,selftest} ...
fail the build when the proof stops matching the code (measure-only)
positional arguments:
{check,source,selftest}
check bind proof constants to runtime constants and compare
source vacuity + docstring checks over Lean sources
selftest positive controls for the checks themselves
options:
-h, --help show this help message and exit
--version show program's version number and exit
proof-drift check¶
$ proof-drift check --help
usage: proof-drift check [-h] --proofs PROOFS --code CODE
[--allow-zero-bindings] [--json]
options:
-h, --help show this help message and exit
--proofs PROOFS directory (or file) of proof sources
--code CODE directory (or file) of runtime sources
--allow-zero-bindings
exit 0 even when ZERO pairs were bound. Default is to
ABSTAIN (exit 2), because a run that compared nothing
has not passed
--json
proof-drift source¶
$ proof-drift source --help
usage: proof-drift source [-h] [--json] files [files ...]
positional arguments:
files
options:
-h, --help show this help message and exit
--json
proof-drift selftest¶
$ proof-drift selftest --help
usage: proof-drift selftest [-h]
options:
-h, --help show this help message and exit
sf-verify¶
$ sf-verify --help
usage: sf-verify [-h] {chain} ...
Re-derive a deployment's recorded admission decisions offline.
positional arguments:
{chain}
chain verify a hash-chained decision log
options:
-h, --help show this help message and exit
sf-verify chain¶
$ sf-verify chain --help
usage: sf-verify chain [-h] [--anchor ANCHOR] [--report REPORT] [--json] log
positional arguments:
log
options:
-h, --help show this help message and exit
--anchor ANCHOR Signed Tree Head. WITHOUT it the verdict is UNVERIFIED,
because tail truncation cannot be detected
--report REPORT write a self-contained HTML report here
--json
signoff-cert¶
$ signoff-cert --help
usage: signoff-cert [-h] [--version] {verify,show,fixtures,conform} ...
reference verifier for signoff-cert/v1 (measure-only)
positional arguments:
{verify,show,fixtures,conform}
verify verify one or more certificates
show print what the certificate says, in English
fixtures write the conformance corpus to disk
conform run the reference verifier against the corpus
options:
-h, --help show this help message and exit
--version show program's version number and exit
signoff-cert verify¶
$ signoff-cert verify --help
usage: signoff-cert verify [-h] [--hmac-key-env HMAC_KEY_ENV]
[--hmac-key-file HMAC_KEY_FILE]
[--pinned-pubkey PINNED_PUBKEY]
[--allow-unauthenticated] [--json]
certs [certs ...]
positional arguments:
certs
options:
-h, --help show this help message and exit
--hmac-key-env HMAC_KEY_ENV
env var holding the shared HMAC key
--hmac-key-file HMAC_KEY_FILE
file holding the shared HMAC key
--pinned-pubkey PINNED_PUBKEY
out-of-band Ed25519 operator public key (hex)
--allow-unauthenticated
check integrity only; the result is NOT attributable
to anyone
--json
signoff-cert show¶
$ signoff-cert show --help
usage: signoff-cert show [-h] cert
positional arguments:
cert
options:
-h, --help show this help message and exit
signoff-cert fixtures¶
$ signoff-cert fixtures --help
usage: signoff-cert fixtures [-h] [--out OUT]
options:
-h, --help show this help message and exit
--out OUT
signoff-cert conform¶
$ signoff-cert conform --help
usage: signoff-cert conform [-h]
options:
-h, --help show this help message and exit
tokencount¶
$ tokencount --help
usage: tokencount [-h] [--version] {count,verify,learn,properties} ...
a token count both parties can recompute (measure-only)
positional arguments:
{count,verify,learn,properties}
count compute the token count
verify check a claimed count
learn learn a merge list from a corpus
properties run the three accounting property checks
options:
-h, --help show this help message and exit
--version show program's version number and exit
tokencount count¶
$ tokencount count --help
usage: tokencount count [-h] [--merges MERGES] text
positional arguments:
text the text, or - for stdin
options:
-h, --help show this help message and exit
--merges MERGES
tokencount verify¶
$ tokencount verify --help
usage: tokencount verify [-h] --claimed CLAIMED [--merges MERGES]
[--tolerance TOLERANCE]
text
positional arguments:
text the text, or - for stdin
options:
-h, --help show this help message and exit
--claimed CLAIMED
--merges MERGES
--tolerance TOLERANCE
tokencount learn¶
$ tokencount learn --help
usage: tokencount learn [-h] [--n N] [--out OUT] corpus
positional arguments:
corpus
options:
-h, --help show this help message and exit
--n N
--out OUT
tokencount properties¶
$ tokencount properties --help
usage: tokencount properties [-h] [--trials TRIALS] [--seed SEED] [--json]
options:
-h, --help show this help message and exit
--trials TRIALS
--seed SEED
--json
Not installed in the environment that built this page
certhead, kvprobe. Their sections are ABSENT rather than described from memory — an invented help text is worse than a gap.