Compile a Lean 4 snippet and return the compiler's verdict. On failure the real error is returned so the agent can repair its own proof. If no Lean toolchain is installed the result is unavailable — never a pass.

Audit #print axioms output against an allowlist. This is the check that catches sorryAx — a development can compile cleanly and still be full of holes, because Lean accepts sorry and exits 0.

What a k-of-n record actually supports, as an exact one-sided Clopper-Pearson bound. 'It passed every time' is not a bound.

Certify that a wait-for relation cannot wedge. Returns the actual cycle when one exists. Supply ranks to also check strict decrease, which is what bounds progress — acyclicity alone only forbids a cycle.

Verify a signoff-cert/v1 certificate: digests, gate consistency, and the false-pass bound RECOMPUTED from the evidence. Requires signoff-cert.

Can a cross-tenant cache probe on this model even be interpreted? Returns failed when the victim's state could not have stayed resident, because a null from an evicted cache is not an all-clear. Requires kvleak.

Before running an experiment, check that its decision rule CAN come out both ways. Returns UNFALSIFIABLE when the finding -- or the null -- can never fire over the declared metric supports. Requires preregister.

How many states must a system distinguish to answer a question about its past? An exact count over an enumerated situation space. Optionally proves a state budget cannot meet it. Requires floorgen.

Exactly how many states does removing a check admit? Replaces 'we found no escapes' with a count. Zero means the check is REDUNDANT, which is a finding. Requires gatecount.

Run every applicable verifier over a directory and aggregate to ONE verdict -- the weakest leg, never the mean. Requires evidence.