Built for agents first. Humans welcome.
https://api.axiom-code.com
Paid endpoints take an API key in the X-API-Key header. Keys are issued after any credit purchase. Trial endpoints take an email address and are limited to 10 verifications with no certificates.
| Method & path | Auth | What it does |
|---|---|---|
POST /v1/trial/verify | Verify a Lean artifact. Returns verdict + transcript. No certificate. 10 lifetime uses per email. | |
POST /v1/verify | API key | Verify and, on pass, issue a signed certificate. Metered by compute time. |
GET /v1/check?serial=... | none | Certificate status: VALID / REVOKED / EXPIRED, with reason. |
GET /v1/revoked | none | The public revocation list. |
GET /v1/account | API key | Credit balance and usage report. |
curl -X POST https://api.axiom-code.com/v1/trial/verify \
-H 'Content-Type: application/json' \
-d '{"email":"you@example.com",
"code":"theorem add_comm_nat (a b : Nat) : a + b = b + a := by\n exact Nat.add_comm a b"}'
# {"verdict":"PASSED","compute_seconds":11.8,"credits_charged":0,
# "trial_remaining":9,"certificate":null,
# "note":"Trial verdicts carry no certificate."}
Endpoint: https://api.axiom-code.com/mcp (streamable HTTP). Tools:
| Tool | What it does |
|---|---|
verify | Submit a Lean artifact; returns verdict, transcript, and (paid) certificate. |
check_certificate | Validate a certificate by serial. |
pricing | Current credit price and pack list. |
usage_report | Metered usage for your API key. |
verify. Ship the certificate with the code — your user can check it without trusting your agent.Compute time is metered at 0.9 credits/second (1 credit = US$0.01). Every response includes compute_seconds and credits_charged. Meter records are append-only and tamper-evident; your usage_report always reconciles.