Documentation

For humans. Agents: see the API reference and llms.txt.

On this page: Writing verifiable specs · Reading verdicts · Certificates · Scope & limits

Writing verifiable specifications

AxiomCode checks Lean 4 artifacts. The unit of verification is one submission: a Lean source file (plus its declared dependencies) with an explicit target the engine should build.

What verifies cleanly

Explicit theorem / def targets with complete proofs.
Statements that say what you mean: name the preconditions, name the postconditions.
Self-contained developments, or ones whose dependencies you declare.

What gets rejected

sorry and admit — placeholders are not proofs. The engine refuses them and tells you exactly where.
Targets that build nothing (vacuous builds).
Anything that doesn’t compile: you get INCOMPLETE with the compiler log, not a pass.

Customer responsibility: the certificate binds the artifact you submitted. It does not certify that your specification captures your intent, or that the deployed system matches the artifact. Writing a faithful spec is your job; checking the proof is ours.

Minimal example

-- A tiny, honest spec: addition commutes on naturals.
theorem add_comm_nat (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b

Submit this in the web verifier: the engine compiles it, the proof checks, the verdict is PASSED.

Reading verdicts

Verdict	Meaning	Certificate?
PASSED	The toolchain compiled the artifact and the proof checked.	Yes (paid only)
FAILED	The proof does not check. The transcript shows why.	No
INCOMPLETE	Doesn’t compile yet, or the target is vacuous. Fix and resubmit.	No

Every verdict ships with the engine transcript and the exact compute time you were charged for.

Certificates

A certificate is a signed JSON document. Fields are defined in the Certificate Policy. Validate any certificate at /check — no account required. Possible outcomes: VALID, REVOKED, EXPIRED.

Scope & limits

Language: Lean 4 only, today.
What “verified” means: the submitted artifact compiled under the stated toolchain and its proofs checked. Nothing about intent, deployment, or the rest of your system.
Validity: 90 days from issuance. Re-verify after changes.
Revocation: if we discover a toolchain or engine defect that undermines a verdict, the certificate is revoked publicly. There is no silent un-verification.