diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..f1fc0e7 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,19 @@ + + +# Changelog + +All notable changes to this project will be documented in this file. + +The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), +and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). + +## [Unreleased] + +### Added +- Portfolio certification rollout (2026-10-05): new `CONTRIBUTING.md` with the standing PR-flow discipline (draft PR → checks green → owner merges; no direct pushes to `main`; CHANGELOG entry under Unreleased + semver bump per PR; releases tagged `vX.Y.Z`); new `NOTICE.md` attribution file; version bumped 0.1.0 → 0.1.1 (patch, chore). +- Flags: publishes are CI-only (GitHub Pages from `docs/`, PyPI publish on release, GitHub release on `v*` tags) — the signed-deploy wrapper currently covers Cloudflare Workers only, so a signed path for these artifacts needs the owner's decision; license headers on existing source files are a follow-up (new files in this PR carry the proprietary header). + +Note: this changelog starts with the current state — earlier history is not reconstructed here. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..ea21477 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,56 @@ + + +# Contributing to AxiomCode + +AxiomCode is proprietary software (see LICENSE — no license is granted without +the copyright holder's prior written permission). Contributions happen by +arrangement with the owner, and every contribution follows the process below. + +## PR-flow discipline (standing rule, 2026-10-05) + +Direct pushes to `main` are retired. Every change lands through a pull request: + +1. Branch off `main` (`git checkout -b /`). +2. Open the PR as a **draft**. +3. Get all checks green (see below), then request review. +4. The **owner merges** — never merge your own PR, never push to `main` directly. +5. Every PR adds a `CHANGELOG.md` entry under `## [Unreleased]` and bumps the + version (patch = fix/chore, minor = feature) in `pyproject.toml`. +6. Merge commits reference the PR number. Releases are tagged `vX.Y.Z` after + merge (the `release` workflow builds and publishes on `v*` tags; the `pypi` + workflow publishes to PyPI on release). + +## Build and test + +```bash +git clone https://github.com/nrupala/axiomcode.git +cd axiomcode +pip install -e ".[dev]" +``` + +Checks (all verified against `.github/workflows/`): + +```bash +# Tests +python -m pytest tests/ -v --tb=short + +# Lint (lint.yml) +ruff check . +ruff format --check . + +# Type check (lint.yml / typecheck.yml) +mypy cli.py core/ --ignore-missing-imports + +# Proof-honesty gate (tests.yml) — lean/src/ must contain no sorry/admit +grep -rEn '\b(sorry|admit)\b' lean/src/ --include='*.lean' && exit 1 || echo "proof-honesty gate: clean" +``` + +Every PR must pass lint, typecheck, tests, and the proof-honesty gate before review. + +## License + +By contributing, you agree your contributions are the proprietary property of +Nrupal Akolkar under the terms in LICENSE. diff --git a/NOTICE.md b/NOTICE.md new file mode 100644 index 0000000..795b9dd --- /dev/null +++ b/NOTICE.md @@ -0,0 +1,10 @@ + + +# NOTICE + +Owned by Nrupal Akolkar · Built with Muse by Meta. + +AxiomCode is proprietary software. No license is granted — see LICENSE. diff --git a/README.md b/README.md index 274a33b..5b49045 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ > **Natural Language to Formally Verified Code** > **Domain:** axiom-code.com -> **Version:** 0.1.0 +> **Version:** 0.1.1 > **License:** Proprietary — see [LICENSE](LICENSE) > **Dependencies:** Zero (pure Python stdlib + cffi) diff --git a/pyproject.toml b/pyproject.toml index 5f737b6..6cfcae7 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "setuptools.build_meta" [project] name = "axiomcode" -version = "0.1.0" +version = "0.1.1" description = "Natural language to formally verified code — zero-trust, encrypted, zero-dependency" readme = "README.md" license = {text = "Proprietary"} @@ -71,6 +71,11 @@ target-version = "py310" [tool.ruff.lint] select = ["E", "F", "I", "N", "W", "UP", "B"] +[tool.ruff.lint.per-file-ignores] +# site generators embed long HTML/CSS template lines; line length is intrinsic there +"site/build.py" = ["E501"] +"site/pages_*.py" = ["E501"] + [tool.mypy] python_version = "3.10" warn_return_any = true diff --git a/services/api/billing.py b/services/api/billing.py index 19082ac..29c7ec8 100644 --- a/services/api/billing.py +++ b/services/api/billing.py @@ -44,7 +44,7 @@ def load_pricing() -> dict: def price_per_compute_s(pricing: dict | None = None) -> float: p = pricing or load_pricing() loaded = sum(v for k, v in p.items() if k != "multiple") - return loaded * p["multiple"] + return float(loaded * p["multiple"]) def charge_for(compute_s: float, pricing: dict | None = None) -> dict: diff --git a/services/api/mcp_server.py b/services/api/mcp_server.py index 16d371e..96b4220 100644 --- a/services/api/mcp_server.py +++ b/services/api/mcp_server.py @@ -21,7 +21,9 @@ from billing import load_keys, meter, price_per_compute_s, usage_for from certs import issue as issue_cert -from mcp.server.fastmcp import FastMCP + +# mcp v1 API; typeshed's mcp.server.fastmcp stub does not declare FastMCP +from mcp.server.fastmcp import FastMCP # type: ignore[attr-defined] from starlette.middleware.base import BaseHTTPMiddleware from starlette.responses import JSONResponse diff --git a/site/README.md b/site/README.md new file mode 100644 index 0000000..3313638 --- /dev/null +++ b/site/README.md @@ -0,0 +1,31 @@ +# axiom-code.com launch site + +Static site for the AxiomCode launch. Vanilla HTML/CSS/JS, no frameworks — +dependency-light and fast. + +## Layout + +- `build.py`, `pages_*.py` — tiny static site generator (page content + shared chrome) +- `run.py` — builds into `dist/` (16 pages + `llms.txt`, `robots.txt`, `sitemap.xml`, + `.well-known/axiomcode.json`, `docs/api/openapi.json`) +- `dist/` — the built site; this is what gets deployed +- `gen_docx.py` — generates `.docx` copies of the paperwork into `paperwork-docx/` +- `paperwork-docx/` — downloadable Word versions of ToS, Privacy, CP/CPS, Refunds, SLA, Security + +## Build + +```bash +python run.py # -> dist/ +python gen_docx.py # -> paperwork-docx/ +``` + +## Deploy + +`dist/` is a static directory — deploy to Cloudflare Pages (or any static host) +with the domain `axiom-code.com`. Before deploy, set in `build.py`: + +- `API_BASE` — the production verification API base URL +- `PADDLE_VENDOR` and `PRICE_IDS` — once the Paddle credit-pack products exist + +The `/verify` and `/check` pages call the API at `API_BASE`; they degrade +gracefully (honest "backend not connected" message) until the backend is live. diff --git a/site/build.py b/site/build.py new file mode 100644 index 0000000..ecbf6f4 --- /dev/null +++ b/site/build.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""AxiomCode launch site generator. Builds static HTML into ./dist.""" + +import html +import json +import os +import shutil + +SITE = "https://axiom-code.com" +NAME = "AxiomCode" +TAGLINE = "The certification authority for software correctness." +HERO_LINE = "Don\u2019t trust our AI \u2014 verify our proof." +API_BASE = "https://api.axiom-code.com" # backend goes live in the next step +PADDLE_VENDOR = 0 # set when Nrupal creates the products +PADDLE_ENV = "production" +PRICE_IDS = { # set when Nrupal creates the products + "starter": "", + "growth": "", + "scale": "", +} + +NAV = [ + ("How it works", "/how-it-works/"), + ("Pricing", "/pricing/"), + ("Docs", "/docs/"), + ("API", "/docs/api/"), + ("Paperwork", "/paperwork/"), +] + +CSS = """ +:root{--ink:#101828;--mut:#475467;--line:#e4e7ec;--paper:#fff;--wash:#f8fafc; +--gold:#b98a2f;--goldsoft:#faf3e3;--green:#12805c;--greensoft:#e9f7f0; +--red:#b42318;--redsoft:#fdeceb;--navy:#0c1f3f;--radius:10px; +--mono:ui-monospace,SFMono-Regular,Menlo,Consolas,monospace; +--sans:-apple-system,BlinkMacSystemFont,"Segoe UI",Inter,Roboto,Helvetica,Arial,sans-serif} +*{box-sizing:border-box}html{scroll-behavior:smooth} +body{margin:0;font-family:var(--sans);color:var(--ink);background:var(--paper);line-height:1.65;font-size:17px} +a{color:#175cd3;text-decoration:none}a:hover{text-decoration:underline} +.wrap{max-width:1080px;margin:0 auto;padding:0 24px} +.prose{max-width:72ch} +/* header */ +.sitehead{border-bottom:1px solid var(--line);background:#fff;position:sticky;top:0;z-index:50} +.sitehead .wrap{display:flex;align-items:center;gap:28px;height:64px} +.brand{display:flex;align-items:center;gap:10px;font-weight:800;font-size:19px;color:var(--ink)} +.brand:hover{text-decoration:none} +.brand svg{width:30px;height:30px} +.nav{display:flex;gap:22px;margin-left:auto;font-size:15px} +.nav a{color:var(--mut)}.nav a:hover{color:var(--ink)} +.cta{display:inline-block;background:var(--navy);color:#fff!important;padding:9px 18px;border-radius:8px;font-weight:600;font-size:15px} +.cta:hover{background:#16294f;text-decoration:none} +/* hero */ +.hero{background:linear-gradient(180deg,#0c1f3f 0%,#12294f 100%);color:#fff;padding:84px 0 72px} +.hero h1{font-size:46px;line-height:1.15;margin:0 0 18px;letter-spacing:-.5px;max-width:16em} +.hero p.lede{font-size:20px;color:#cbd5e1;max-width:34em;margin:0 0 28px} +.hero .row{display:flex;gap:14px;flex-wrap:wrap} +.btn{display:inline-block;padding:13px 26px;border-radius:9px;font-weight:700;font-size:16px;border:1px solid transparent} +.btn-gold{background:var(--gold);color:#1a1206!important}.btn-gold:hover{background:#c99a3f;text-decoration:none} +.btn-ghost{border-color:#3b4a63;color:#fff!important}.btn-ghost:hover{border-color:#5b6b85;text-decoration:none} +.trustline{margin-top:26px;font-size:14px;color:#93a1b8} +/* sections */ +section.block{padding:64px 0} +section.block h2{font-size:30px;margin:0 0 12px;letter-spacing:-.3px} +.kicker{font-size:13px;font-weight:700;letter-spacing:1.5px;text-transform:uppercase;color:var(--gold);margin-bottom:8px} +.cards{display:grid;grid-template-columns:repeat(auto-fit,minmax(280px,1fr));gap:20px;margin-top:28px} +.card{border:1px solid var(--line);border-radius:var(--radius);padding:26px;background:#fff} +.card h3{margin:0 0 8px;font-size:19px} +.card p{margin:0;color:var(--mut);font-size:15.5px} +.card .num{display:inline-flex;width:34px;height:34px;border-radius:50%;background:var(--navy);color:#fff; +align-items:center;justify-content:center;font-weight:700;margin-bottom:12px} +/* seal / cert demo */ +.sealbox{background:var(--wash);border:1px solid var(--line);border-radius:12px;padding:28px;margin-top:24px} +pre.code{background:#0c1f3f;color:#d7e3f4;padding:20px;border-radius:10px;overflow:auto;font-size:14px;line-height:1.55;font-family:var(--mono)} +code.inline{font-family:var(--mono);background:var(--wash);border:1px solid var(--line);border-radius:5px;padding:1px 7px;font-size:.88em} +/* verdict badges */ +.badge{display:inline-block;padding:4px 14px;border-radius:999px;font-weight:700;font-size:14px} +.b-pass{background:var(--greensoft);color:var(--green);border:1px solid #bfe6d2} +.b-fail{background:var(--redsoft);color:var(--red);border:1px solid #f3c2bc} +.b-warn{background:var(--goldsoft);color:#8a6414;border:1px solid #ecd9a8} +/* pricing */ +.ptable{display:grid;grid-template-columns:repeat(auto-fit,minmax(240px,1fr));gap:18px;margin-top:28px} +.plan{border:1px solid var(--line);border-radius:12px;padding:28px;background:#fff;position:relative} +.plan.hot{border:2px solid var(--gold);box-shadow:0 8px 30px rgba(185,138,47,.12)} +.plan h3{margin:0 0 4px}.plan .price{font-size:34px;font-weight:800;margin:8px 0} +.plan .per{color:var(--mut);font-size:14px} +.plan ul{padding-left:20px;color:var(--mut);font-size:15px;margin:16px 0} +.plan li{margin-bottom:8px} +/* forms */ +textarea.codebox{width:100%;min-height:260px;font-family:var(--mono);font-size:14px;padding:16px; +border:1px solid var(--line);border-radius:10px;background:#fbfcfe;resize:vertical} +input[type=text],input[type=email]{width:100%;padding:12px 14px;border:1px solid var(--line);border-radius:8px;font-size:16px} +label.fl{display:block;font-weight:600;margin:18px 0 6px} +button.go{background:var(--navy);color:#fff;border:0;padding:13px 30px;border-radius:9px;font-size:16px;font-weight:700;cursor:pointer} +button.go:hover{background:#16294f}button.go:disabled{opacity:.55;cursor:wait} +.result{margin-top:24px;border:1px solid var(--line);border-radius:10px;padding:22px;display:none} +.result.show{display:block} +/* footer */ +.sitefoot{background:#0c1f3f;color:#aeb9cc;padding:56px 0 32px;margin-top:40px;font-size:15px} +.sitefoot a{color:#d7e0ee}.sitefoot .cols{display:grid;grid-template-columns:repeat(auto-fit,minmax(200px,1fr));gap:28px} +.sitefoot h4{color:#fff;margin:0 0 12px;font-size:15px} +.sitefoot ul{list-style:none;margin:0;padding:0}.sitefoot li{margin-bottom:8px} +.fine{margin-top:36px;padding-top:20px;border-top:1px solid #22345a;font-size:13px;color:#7d8ba3} +/* docs */ +.docnav{background:var(--wash);border:1px solid var(--line);border-radius:10px;padding:18px 22px;margin:24px 0} +table.spec{width:100%;border-collapse:collapse;font-size:15px;margin:20px 0} +table.spec th,table.spec td{border:1px solid var(--line);padding:10px 14px;text-align:left;vertical-align:top} +table.spec th{background:var(--wash)} +.note{border-left:4px solid var(--gold);background:var(--goldsoft);padding:14px 18px;border-radius:0 8px 8px 0;margin:20px 0;font-size:15.5px} +.note.blue{border-color:#175cd3;background:#eff4ff} +h1.pt{font-size:38px;letter-spacing:-.4px;margin:0 0 10px} +.sub{color:var(--mut);font-size:19px;margin:0 0 8px} +.faq details{border:1px solid var(--line);border-radius:8px;padding:14px 18px;margin-bottom:10px} +.faq summary{font-weight:700;cursor:pointer} +@media(max-width:760px){.hero h1{font-size:32px}.nav{display:none}} +""" + +SEAL_SVG = """""" + + +def head(title, desc, path, extra_jsonld=None): + canon = SITE + path + jl = "" + if extra_jsonld: + jl = '" + return f""" + + + + +{html.escape(title)} | AxiomCode + + + + + + + + + + + +{jl} + + +""" + + +def header(active=""): + links = [] + for label, href in NAV: + links.append(f'{label}') + return f"""
+{SEAL_SVG}AxiomCode + +Try free +
+""" + + +FOOTER = """ + +""" + +PAGES: list = [] # (path, title, desc, body_html, jsonld) + + +def page(path, title, desc, body, jsonld=None): + PAGES.append((path, title, desc, body, jsonld)) + + +def render_all(outdir): + if os.path.exists(outdir): + shutil.rmtree(outdir) + for path, title, desc, body, jsonld in PAGES: + full = os.path.join(outdir, path.lstrip("/")) + os.makedirs(full, exist_ok=True) + with open(os.path.join(full, "index.html"), "w") as f: + f.write(head(title, desc, path, jsonld) + header() + body + FOOTER) + # root-level files + with open(os.path.join(outdir, "robots.txt"), "w") as f: + f.write("User-agent: *\nAllow: /\n\nSitemap: " + SITE + "/sitemap.xml\n") + urls = [p for p, _, _, _, _ in PAGES] + sm = ['', ''] + for u in urls: + sm.append(f" {SITE}{u}weekly") + sm.append("") + with open(os.path.join(outdir, "sitemap.xml"), "w") as f: + f.write("\n".join(sm)) + print(f"rendered {len(PAGES)} pages -> {outdir}") diff --git a/site/dist/.well-known/axiomcode.json b/site/dist/.well-known/axiomcode.json new file mode 100644 index 0000000..590ad26 --- /dev/null +++ b/site/dist/.well-known/axiomcode.json @@ -0,0 +1,18 @@ +{ + "service": "AxiomCode", + "description": "Certification authority for software correctness. Machine-checked proofs, signed certificates.", + "homepage": "https://axiom-code.com", + "api_base": "https://api.axiom-code.com", + "mcp": "https://api.axiom-code.com/mcp", + "llms_txt": "https://axiom-code.com/llms.txt", + "docs": "https://axiom-code.com/docs/api/", + "certificate_checker": "https://axiom-code.com/check/", + "revocation_list": "https://api.axiom-code.com/v1/revoked", + "ca_public_keys": "https://axiom-code.com/.well-known/axiomcode-keys.json", + "pricing": "https://axiom-code.com/pricing/", + "trial": { + "verifications": 10, + "certificates": false + }, + "contact": "hello@axiom-code.com" +} \ No newline at end of file diff --git a/site/dist/blog/dont-trust-our-ai/index.html b/site/dist/blog/dont-trust-our-ai/index.html new file mode 100644 index 0000000..466ee08 --- /dev/null +++ b/site/dist/blog/dont-trust-our-ai/index.html @@ -0,0 +1,172 @@ + + + + + +Don’t trust our AI — verify our proof | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
26 September 2026 · Launch
+

Don’t trust our AI — verify our proof

+

Why we built a certification authority for software correctness.

+ +

AI writes code now. A lot of it. And the industry’s answer to “is it right?” is still, essentially, vibes: code review (opinion), tests (samples), audits (expensive snapshots). All useful. None of them evidence.

+ +

We started AxiomCode with a different premise: correctness should be certifiable the way identity is. When you visit your bank, you don’t read the bank’s audit report — your browser checks a certificate issued by an authority whose entire business is not lying about identity. Software needs the same thing for correctness: a party whose business is not lying about verification.

+ +

Verification-as-evidence, not verification-as-opinion

+

An AI code reviewer gives you an opinion. AxiomCode gives you evidence: the artifact hash, the toolchain that ran, the transcript of the check, sealed under our signature. You don’t have to believe us — or our AI. Re-run the check yourself. The certificate tells you exactly what was verified and how.

+ +

The trial gives you everything except the certificate

+

Try us free: 10 verifications, real verdicts, real transcripts. But no certificates. That isn’t stinginess — it’s the business model working as designed. A certificate says we stake our name on this verdict. Staking our name costs real money: the compute, the operations, the insurance, the revocation infrastructure, the people who answer when something goes wrong. We only stake it inside a commercial relationship where those costs are covered. A free certificate would be a souvenir. Ours is a trust instrument.

+ +

The one risk we organize around

+

A certification authority has exactly one existential risk: mis-issuance — saying “verified” when it isn’t. Everything about the design flows from that: the engine rejects sorry, admit, vacuous builds, and broken proofs loudly. Certificates expire in 90 days so evidence stays fresh. And if our toolchain is ever wrong, we revoke publicly — there is no silent un-verification. Like TLS, but for correctness.

+ +

Who it’s for

+

Whoever has to prove correctness to a third party: regulated teams facing auditors, fintech and smart-contract builders moving money, agent builders whose agents ship code, procurement teams who want “certified correct” as a deliverable. If you’re that person, run your first verification free. Don’t trust our AI — verify our proof.

+
+ + + \ No newline at end of file diff --git a/site/dist/blog/index.html b/site/dist/blog/index.html new file mode 100644 index 0000000..b1e4112 --- /dev/null +++ b/site/dist/blog/index.html @@ -0,0 +1,149 @@ + + + + + +Blog | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

Blog

+

Notes on verification-as-evidence and building a certification authority for software.

+
+
26 September 2026
+

Don’t trust our AI — verify our proof

+

Why we built a certification authority for software correctness, why the trial gives you everything except the certificate, and why mis-issuance — saying “verified” when it isn’t — is the one risk we organize the whole company around.

+
+
+ + + \ No newline at end of file diff --git a/site/dist/check/index.html b/site/dist/check/index.html new file mode 100644 index 0000000..7fb440b --- /dev/null +++ b/site/dist/check/index.html @@ -0,0 +1,176 @@ + + + + + +Check a certificate | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

Check a certificate

+

No account needed. Paste the certificate JSON — we’ll tell you if it’s VALID, REVOKED, or EXPIRED, and why.

+ + +

+
+
Don’t trust our AI — verify our proof. A certificate is only as good as its checkability. This page, the API, and the published revocation list are how you hold us accountable.
+
+ + + + \ No newline at end of file diff --git a/site/dist/docs/api/index.html b/site/dist/docs/api/index.html new file mode 100644 index 0000000..a0d0402 --- /dev/null +++ b/site/dist/docs/api/index.html @@ -0,0 +1,192 @@ + + + + + +REST & MCP API | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

REST & MCP API

+

Built for agents first. Humans welcome.

+
Machine-readable:  llms.txt · /.well-known/axiomcode.json · OpenAPI (JSON)
+ +

Base URL

+

https://api.axiom-code.com

+ +

Authentication

+

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.

+ +

REST endpoints

+ + + + + + + +
Method & pathAuthWhat it does
POST /v1/trial/verifyemailVerify a Lean artifact. Returns verdict + transcript. No certificate. 10 lifetime uses per email.
POST /v1/verifyAPI keyVerify and, on pass, issue a signed certificate. Metered by compute time.
GET /v1/check?serial=...noneCertificate status: VALID / REVOKED / EXPIRED, with reason.
GET /v1/revokednoneThe public revocation list.
GET /v1/accountAPI keyCredit balance and usage report.
+ +

Example: trial verification

+
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."}
+ +

MCP server

+

Endpoint: https://api.axiom-code.com/mcp (streamable HTTP). Tools:

+ + + + + + +
ToolWhat it does
verifySubmit a Lean artifact; returns verdict, transcript, and (paid) certificate.
check_certificateValidate a certificate by serial.
pricingCurrent credit price and pack list.
usage_reportMetered usage for your API key.
+
Agent pattern: after your coding agent finishes a safety-critical function, have it write the Lean spec and call verify. Ship the certificate with the code — your user can check it without trusting your agent.
+ +

Metering

+

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.

+ +

Rate limits & abuse

+
    +
  • Trial: 10 verifications per email, lifetime; 1 concurrent request.
    • +
  • Paid: 5 concurrent verifications per key by default; contact us for more.
    • +
  • Submissions are capped at 2 MB of source; engine time is capped per call.
    • +
  • We may suspend keys used to probe the engine adversarially or to resell trial access. See the Terms.
    • +
+
+ + + \ No newline at end of file diff --git a/site/dist/docs/api/openapi.json b/site/dist/docs/api/openapi.json new file mode 100644 index 0000000..64ea2d7 --- /dev/null +++ b/site/dist/docs/api/openapi.json @@ -0,0 +1,40 @@ +{ + "openapi": "3.0.3", + "info": { + "title": "AxiomCode API", + "version": "1.0.0", + "description": "Verification and certification API. Full reference at https://axiom-code.com/docs/api/" + }, + "servers": [ + { + "url": "https://api.axiom-code.com" + } + ], + "paths": { + "/v1/trial/verify": { + "post": { + "summary": "Trial verification (email, 10 lifetime, no certificate)" + } + }, + "/v1/verify": { + "post": { + "summary": "Paid verification with certificate (API key)" + } + }, + "/v1/check": { + "get": { + "summary": "Certificate status by serial (no auth)" + } + }, + "/v1/revoked": { + "get": { + "summary": "Public revocation list (no auth)" + } + }, + "/v1/account": { + "get": { + "summary": "Balance and usage (API key)" + } + } + } +} \ No newline at end of file diff --git a/site/dist/docs/index.html b/site/dist/docs/index.html new file mode 100644 index 0000000..3a96ad1 --- /dev/null +++ b/site/dist/docs/index.html @@ -0,0 +1,188 @@ + + + + + +Documentation | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

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

+ + + + + +
VerdictMeaningCertificate?
PASSEDThe toolchain compiled the artifact and the proof checked.Yes (paid only)
FAILEDThe proof does not check. The transcript shows why.No
INCOMPLETEDoesn’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 certificate credentials the code — our assessment that the submitted artifact was built to its specification, as mechanically checked. We hold no responsibility beyond this assessment. 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.
    • +
+
+ + + \ No newline at end of file diff --git a/site/dist/how-it-works/index.html b/site/dist/how-it-works/index.html new file mode 100644 index 0000000..eeee262 --- /dev/null +++ b/site/dist/how-it-works/index.html @@ -0,0 +1,180 @@ + + + + + +How it works | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

How it works

+

Three steps. Every one of them checkable.

+ +

1. Submit the artifact

+

Paste Lean 4 code into the web verifier, POST it to the REST API, or call the verify tool on our MCP server. What you submit is hashed (SHA-256) the moment it arrives — that hash becomes part of the certificate, so the verdict can never drift away from the code it describes.

+ +

2. The engine checks the proof — for real

+

The verification engine runs the actual Lean toolchain (lake build) against your artifact in an isolated project. It is deliberately adversarial toward sloppy proofs:

+
    +
  • Vacuous builds rejected. A target that compiles nothing is not a proof of anything.
    • +
  • sorry and admit rejected. Placeholders are not proofs.
    • +
  • Broken proofs rejected. If the toolchain reports an error, the verdict is FAILED, with the log attached.
    • +
  • Unfinished work reported honestly. Something that doesn’t compile yet gets INCOMPLETE — never a pass.
    • +
+

A pass means one thing: the toolchain compiled your artifact and the proof checked. The full transcript ships with the verdict.

+ +

3. The certificate seals the evidence

+

On PASSED, the certification authority issues a signed certificate. The certificate credentials the code — our assessment that the artifact was built to its specification, as mechanically checked — and we hold no responsibility beyond this assessment. It contains:

+ + + + + + + + + +
FieldMeaning
artifact_sha256Hash of exactly the code that was checked
verdictPASSED, with the toolchain transcript reference
toolchainLean / lake versions that ran the check
issuerAxiomCode CA
serialUnique serial number
validity90-day window (notBefore / notAfter)
signatureCA signature over all of the above
+
+

Check any certificate, no account needed: paste it into the certificate checker. You’ll get VALID, REVOKED, or EXPIRED — with the reason. Revocation is published, not hidden: if a toolchain bug ever invalidates a verdict, the serial goes on the public revocation list.

+
+ +

Interfaces

+ +
+ + + \ No newline at end of file diff --git a/site/dist/index.html b/site/dist/index.html new file mode 100644 index 0000000..f1f0dcf --- /dev/null +++ b/site/dist/index.html @@ -0,0 +1,202 @@ + + + + + +Software correctness, certified | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

Don’t trust our AI — verify our proof.

+

The certification authority for software correctness. Submit your specification. Our engine compiles it, checks the proof mechanically, and issues a signed certificate — binding your code hash, the verification result, and our identity — that anyone can re-check without trusting us.

+
+Verify something free +How it works +
+

10 free trial verifications · no certificate until you pay · certificates valid 90 days, revocable, publicly checkable

+
+ +
+
The problem
+

AI writes code. Nobody can prove it’s right.

+

Code review is opinion. Tests are samples. Audits are expensive snapshots. When software has to be right — money movement, access control, safety logic, smart contracts — “looks good to me” is not evidence. AxiomCode sells verification-as-evidence: a mechanical proof, checked by a real toolchain, sealed into a certificate you can hand to a regulator, a customer, or a counterparty.

+
+
+
1

Submit

Send a Lean 4 specification through the web UI, the REST API, or the MCP server — the way your agent already talks to tools.

+
2

We check it mechanically

The engine compiles your spec with the real Lean toolchain and checks the proof. Vacuous builds, sorry, admit, and broken proofs are rejected — loudly.

+
3

You get a certificate

A signed certificate binding your artifact hash, the verdict, the toolchain, the issuer, and a validity window. Anyone can re-verify it without trusting us.

+
+
+ +
+
The guarantee
+

Our honesty is structural, not promised.

+

A certificate authority lives or dies on one thing: never saying “verified” when it isn’t. So we built the incentives into the system:

+
+
+

Mis-issuance is the existential risk

Every certificate carries a serial number, issuer identity, and validity window. If our toolchain is ever wrong, we revoke — publicly, through a published revocation list. Like TLS, but for correctness.

+

Expiry drives re-verification

Certificates last 90 days. Software changes; proofs should be re-run. Renewal is the business model, the same way TLS renewal is.

+

You don’t have to trust us

The certificate binds the artifact hash and the proof transcript. Re-run the check yourself with the published toolchain. “Don’t trust our AI — verify our proof” isn’t a slogan; it’s the architecture.

+
+
+ +
+
Who it’s for
+

Whoever has to prove it’s correct.

+

The buyer isn’t whoever writes the code. It’s whoever must demonstrate correctness to a third party:

+
    +
  • Regulated software teams — hand a certificate to the auditor instead of a test report.
    • +
  • Fintech & smart contracts — money logic with a machine-checked proof attached.
    • +
  • AI agent builders — agents that ship code can now ship the proof too. Call us from your agent over MCP.
    • +
  • Procurement & contracts — “certified correct” as a deliverable, checkable by the buyer.
    • +
+

See pricing

+
+ +
+
Honest scope
+

What we certify today — and what we don’t.

+

Today the engine verifies Lean 4 specifications. The certificate credentials the code: it is our assessment that the submitted artifact was built to its specification, as mechanically checked — recorded as the artifact hash, the toolchain version, and the verdict. We hold no responsibility beyond this assessment. We do not claim your whole system is correct, your spec matches your intent, or your deployment matches the artifact. Read the Certificate Policy for the precise meaning of every field.

+
Verification is evidence, not opinion. The evidence is bounded, and we publish the bounds.
+
+ + + \ No newline at end of file diff --git a/site/dist/llms.txt b/site/dist/llms.txt new file mode 100644 index 0000000..92bdab6 --- /dev/null +++ b/site/dist/llms.txt @@ -0,0 +1,38 @@ +# AxiomCode + +> The certification authority for software correctness. Don't trust our AI — verify our proof. + +AxiomCode verifies Lean 4 software specifications with a real toolchain and issues +signed, revocable, independently verifiable certificates binding the artifact hash, +verdict, toolchain, issuer, serial, and validity window. + +## For agents + +- API docs: https://axiom-code.com/docs/api/ +- Machine-readable service info: https://axiom-code.com/.well-known/axiomcode.json +- REST base: https://api.axiom-code.com +- MCP server: https://api.axiom-code.com/mcp with tools: verify, check_certificate, pricing, usage_report +- Check any certificate (no auth): GET https://api.axiom-code.com/v1/check?serial=... +- Revocation list: https://api.axiom-code.com/v1/revoked + +## Trial + +10 free verifications per email via POST /v1/trial/verify. Trial verdicts include the +verdict and transcript but NEVER a certificate. Certificates are issued to paying +customers only (credit packs from $10; 1 credit = $0.01; metered at 0.9 credits/sec +of engine compute time). + +## Scope (honest) + +Today: Lean 4 only. A PASSED verdict means the submitted artifact compiled under the +stated toolchain and its proofs checked. It does not certify intent, deployment, or +the rest of the system. Certificates are valid 90 days and revocable. Mis-issuance +is handled by public revocation — see the Certificate Policy. + +## Paperwork + +- Terms: https://axiom-code.com/paperwork/terms/ +- Privacy: https://axiom-code.com/paperwork/privacy/ +- Certificate Policy & CPS: https://axiom-code.com/paperwork/certificate-policy/ +- Refunds: https://axiom-code.com/paperwork/refunds/ +- Security & disclosure: https://axiom-code.com/paperwork/security/ diff --git a/site/dist/paperwork/certificate-policy/index.html b/site/dist/paperwork/certificate-policy/index.html new file mode 100644 index 0000000..c1d0f43 --- /dev/null +++ b/site/dist/paperwork/certificate-policy/index.html @@ -0,0 +1,168 @@ + + + + + +Certificate Policy & Certification Practice Statement | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+

Certificate Policy & Certification Practice Statement

Last updated: 26 September 2026

Download as Word (.docx)

This document follows the structure of RFC 3647. It states what AxiomCode certificates mean, how they are issued, and what happens when something goes wrong. It should be reviewed by qualified legal counsel and a PKI auditor before certificates are relied upon in regulated contexts.

+

1. Introduction

+

1.1 Overview. AxiomCode operates a certification authority (“AxiomCode CA”) that issues certificates binding a software artifact’s hash to a machine-checked verification verdict. Verification-as-evidence, not verification-as-opinion: every certificate carries the evidence needed to re-check it.

+

1.2 Document name. AxiomCode Certificate Policy and Certification Practice Statement, version 1.0 (2026-09-26).

+

1.3 Participants. The CA (AxiomCode), subscribers (paying customers who request verification), and relying parties (anyone who validates a certificate).

+

1.4 Certificate usage. Each certificate credentials the code submitted: it is our assessment that the artifact with the stated hash was built to its specification, as mechanically checked by the stated toolchain on the stated date. We hold no responsibility beyond this assessment. Appropriate uses: audit evidence, procurement deliverables, counterparty assurance. Prohibited reliance: treating a certificate as a warranty of safety, fitness, or intent — see §9.

+

2. Publication

+

The CP/CPS, the CA’s public verification keys, and the revocation list are published at axiom-code.com and queryable without an account.

+

3. Identification and authentication

+

Subscribers are identified by account (email + API key). Artifacts are identified by SHA-256 hash computed at submission. No identity vetting of persons is performed: the certificate speaks about the artifact, not the author.

+

4. Certificate life-cycle

+

4.1 Application. A paid verification request is a certificate application. Trial requests are never applications — no certificate can result.

+

4.2 Issuance. On a PASSED verdict, the CA signs a certificate containing artifact hash, verdict, toolchain versions, issuer name, unique serial, and a 90-day validity window. FAILED and INCOMPLETE verdicts produce no certificate, ever.

+

4.3 Validity and renewal. 90 days from issuance. Renewal is re-verification at the standard credit meter — there is no shortcut renewal, because the point is fresh evidence.

+

4.4 Revocation. The CA revokes a certificate when: (a) a toolchain or engine defect undermines the verdict; (b) the certificate was mis-issued; (c) the subscriber requests it. Revocations are published to the revocation list promptly (target: within 24 hours of the decision) and are permanent.

+

4.5 Incident handling. Suspected mis-issuance triggers an internal review; confirmed mis-issuance triggers revocation, a public incident note, and re-verification of affected artifacts at our expense. Mis-issuance is treated as the CA’s existential risk.

+

5. Operational controls

+

Verification runs in isolated, single-use build environments. CA signing keys are segregated from the web/API tier; signing requires the isolated CA service. All issuance, revocation, and metering events are written to a tamper-evident append-only log.

+

6. Technical security controls

+

Certificates are signed with modern asymmetric signatures (Ed25519); the CA’s public keys are published for independent verification. Key generation uses a vetted CSPRNG; private keys are access-controlled and backed up encrypted. Key compromise triggers key rollover, re-issuance of affected certificates, and public disclosure.

+

7. Certificate and revocation profiles

+

Certificates are signed JSON documents with the fields listed in How it works §3. The revocation list is a signed JSON document listing revoked serials with reason codes and timestamps, updated on every revocation.

+

8. Compliance

+

We log every issuance and revocation; logs are available to auditors under NDA. Annual self-assessment against this CP/CPS is published in summary form.

+

9. Legal matters

+

Certificates credential the code submitted and nothing more; they are factual statements about a verification event, not warranties. We hold no responsibility beyond the assessment stated in the certificate. Liability is limited as stated in the Terms of Service (per-certificate cap at the verification fee; aggregate cap at 12 months’ fees; no consequential damages; no duty to relying parties beyond this Policy). Subscribers warrant they have the right to submit the artifact. Relying parties must validate certificates through the published checker and revocation list before relying; any reliance is at the relying party’s own risk.

+
+ + \ No newline at end of file diff --git a/site/dist/paperwork/index.html b/site/dist/paperwork/index.html new file mode 100644 index 0000000..4fc0cd9 --- /dev/null +++ b/site/dist/paperwork/index.html @@ -0,0 +1,152 @@ + + + + + +Trust & paperwork | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+

Trust & paperwork

Last updated: 26 September 2026

Everything that governs the service, in one place.

+ +

Downloadable Word copies of each document are linked at the top of each page.

+
+ + \ No newline at end of file diff --git a/site/dist/paperwork/paperwork-certificate-policy.docx b/site/dist/paperwork/paperwork-certificate-policy.docx new file mode 100644 index 0000000..12bc2df Binary files /dev/null and b/site/dist/paperwork/paperwork-certificate-policy.docx differ diff --git a/site/dist/paperwork/paperwork-privacy.docx b/site/dist/paperwork/paperwork-privacy.docx new file mode 100644 index 0000000..71d3e5f Binary files /dev/null and b/site/dist/paperwork/paperwork-privacy.docx differ diff --git a/site/dist/paperwork/paperwork-refunds.docx b/site/dist/paperwork/paperwork-refunds.docx new file mode 100644 index 0000000..4c19128 Binary files /dev/null and b/site/dist/paperwork/paperwork-refunds.docx differ diff --git a/site/dist/paperwork/paperwork-security.docx b/site/dist/paperwork/paperwork-security.docx new file mode 100644 index 0000000..4801c76 Binary files /dev/null and b/site/dist/paperwork/paperwork-security.docx differ diff --git a/site/dist/paperwork/paperwork-sla.docx b/site/dist/paperwork/paperwork-sla.docx new file mode 100644 index 0000000..ae51919 Binary files /dev/null and b/site/dist/paperwork/paperwork-sla.docx differ diff --git a/site/dist/paperwork/paperwork-terms.docx b/site/dist/paperwork/paperwork-terms.docx new file mode 100644 index 0000000..6876ccd Binary files /dev/null and b/site/dist/paperwork/paperwork-terms.docx differ diff --git a/site/dist/paperwork/privacy/index.html b/site/dist/paperwork/privacy/index.html new file mode 100644 index 0000000..88d5781 --- /dev/null +++ b/site/dist/paperwork/privacy/index.html @@ -0,0 +1,162 @@ + + + + + +Privacy Policy | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+

Privacy Policy

Last updated: 26 September 2026

Download as Word (.docx)

1. What we collect

+
    +
  • Submitted artifacts: the code you ask us to verify, its SHA-256 hash, the verdict, and the engine transcript. We cannot verify without it.
    • +
  • Account data: email address, API keys, credit balance, and purchase records from our merchant of record.
    • +
  • Metering records: compute time, credits charged, timestamps — kept in a tamper-evident log so your bill always reconciles.
    • +
  • Operational logs: IP addresses and request metadata for abuse prevention, kept briefly.
    • +
+

2. What we never do

+

We never sell your data. We never use your submitted code to train models. We never disclose your artifacts except as needed to operate the service (e.g., payment processing by our merchant of record) or as required by law.

+

3. Why certificates are public-ish

+

A certificate is useful precisely because third parties can check it. Certificate contents (artifact hash, verdict, toolchain, serial, validity) and the revocation list are queryable by anyone. The artifact source itself is not published — only its hash.

+

4. Retention and deletion

+
    +
  • Artifacts and transcripts: retained while your account is active, to support re-verification and dispute handling; deleted within 90 days of account closure on request.
    • +
  • Metering and purchase records: retained as required for tax and accounting (typically 7 years), in anonymized form where possible after closure.
    • +
  • Operational logs: 30 days.
    • +
+

To request deletion or a copy of your data: hello@axiom-code.com. Some records (revoked certificate entries, tax records) cannot be deleted while the law requires them.

+

5. Security

+

CA signing keys are held separately from the web service with restricted access; see Security. No method is perfect; we disclose breaches affecting your data promptly.

+
+ + \ No newline at end of file diff --git a/site/dist/paperwork/refunds/index.html b/site/dist/paperwork/refunds/index.html new file mode 100644 index 0000000..7863260 --- /dev/null +++ b/site/dist/paperwork/refunds/index.html @@ -0,0 +1,157 @@ + + + + + +Billing, trial & refund policy | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+

Billing, trial & refund policy

Last updated: 26 September 2026

Download as Word (.docx)

1. Trial

+

Every new email address gets 10 free verifications. Trial verdicts include the verdict and transcript but never a certificate. The trial demonstrates the engine; certification is the paid product. One trial per person; creating multiple accounts to harvest trials is abuse and will be suspended.

+

2. Credits

+
    +
  • 1 credit = US$0.01. Packs: Starter $10 (1,000 credits), Growth $50 (5,000), Scale $200 (20,000).
    • +
  • Verification consumes credits by engine compute time at 0.9 credits/second, shown with every verdict and itemized in your usage report.
    • +
  • Credits never expire and are not transferable between accounts.
    • +
  • Payment is processed by our merchant of record (Paddle); we never see or store your card.
    • +
+

3. Refunds

+

Unused credits are refundable within 14 days of purchase — email hello@axiom-code.com and we return the unused portion to the original payment method. Credits already consumed by verifications are not refundable: the compute was spent and the evidence delivered. Genuine metering errors are always corrected with credit, no time limit.

+

4. Cancellation

+

There are no subscriptions to cancel — credits are prepaid. Stop buying packs whenever you like; your balance, certificates, and history remain available.

+

5. Disputes

+

Dispute a charge within 30 days with the serial numbers or timestamps involved; we investigate against the tamper-evident meter log, which is the record of truth both sides can inspect.

+
+ + \ No newline at end of file diff --git a/site/dist/paperwork/security/index.html b/site/dist/paperwork/security/index.html new file mode 100644 index 0000000..118ca7d --- /dev/null +++ b/site/dist/paperwork/security/index.html @@ -0,0 +1,156 @@ + + + + + +Security & responsible disclosure | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+

Security & responsible disclosure

Last updated: 26 September 2026

Download as Word (.docx)

1. How we protect the CA

+
    +
  • Key segregation: CA signing keys live in an isolated service, separate from the web and API tiers. The public internet never touches the signer.
    • +
  • Least privilege: few humans can touch the CA; every touch is logged.
    • +
  • Tamper-evident logs: issuance, revocation, and metering are append-only and hash-chained. If the log doesn’t reconcile, we treat it as an incident.
    • +
  • Isolated builds: every verification runs in a single-use environment; artifacts can’t see each other or the host.
    • +
  • Dependency hygiene: the Lean toolchain is pinned; upgrades are tested against the regression suite before they touch production verdicts.
    • +
+

2. Responsible disclosure

+

Found a vulnerability? Email security@axiom-code.com with the details and a way to reach you. We ask for a reasonable window (90 days) before public disclosure so we can fix, revoke affected certificates if needed, and publish an incident note. We commit to acknowledging within 2 business days and keeping you updated.

+

3. Scope

+

In scope: the API, the MCP server, the certificate checker, the CA issuance path, and this site. Out of scope: third-party services (Paddle, Cloudflare), social engineering, and physical attacks. Please don’t disrupt the service or access other customers’ data while researching.

+

4. What we won’t do

+

We won’t threaten researchers who follow this policy, and we won’t ask law enforcement to chill good-faith research. If you’re unsure whether something is in scope, ask first.

+
+ + \ No newline at end of file diff --git a/site/dist/paperwork/sla/index.html b/site/dist/paperwork/sla/index.html new file mode 100644 index 0000000..99ca633 --- /dev/null +++ b/site/dist/paperwork/sla/index.html @@ -0,0 +1,154 @@ + + + + + +Service levels & support | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+

Service levels & support

Last updated: 26 September 2026

Download as Word (.docx)

1. Uptime

+

Target: 99% monthly availability for the API and certificate checker, excluding scheduled maintenance (announced 48h ahead) and upstream outages. The static site and published revocation list are served from the edge and targeted higher, but the commitment we make is 99% on the API.

+

2. Verification queue

+

Verifications normally start within 60 seconds. At high load, paid verifications queue ahead of trial verifications, and Scale customers queue ahead of others. Engine time per call is capped; very large artifacts may be asked to split submissions.

+

3. Support

+
    +
  • Email: hello@axiom-code.com — target first response 1 business day.
    • +
  • Mis-issuance / revocation issues: treated as critical; target acknowledgment 4 business hours.
    • +
  • Docs and status: this site’s documentation; a status page ships with the production rollout.
    • +
+

4. Remedies

+

If monthly API availability falls below 99%, affected paying customers receive a 10% credit rebate for the month, applied automatically. This is our sole remedy for downtime and is without prejudice to the liability limits in the Terms.

+
+ + \ No newline at end of file diff --git a/site/dist/paperwork/terms/index.html b/site/dist/paperwork/terms/index.html new file mode 100644 index 0000000..40c0c85 --- /dev/null +++ b/site/dist/paperwork/terms/index.html @@ -0,0 +1,160 @@ + + + + + +Terms of Service | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+

Terms of Service

Last updated: 26 September 2026

Download as Word (.docx)

1. The service

+

AxiomCode (“we”) provides machine-checked verification of software specifications and issues signed certificates recording the verification outcome (“certificates”). The service is offered through a web interface, a REST API, and an MCP server.

+

2. Trial

+

New users may run up to 10 trial verifications without payment. Trial verdicts include the verdict and the engine transcript; trial verdicts never include certificates. Trial access is rate-limited and may not be resold, shared across accounts to evade the limit, or used to probe the engine adversarially.

+

3. Credits and payment

+

Paid verification consumes credits (1 credit = US$0.01), metered by engine compute time at the published rate. Credits are purchased in packs through our merchant of record and never expire. Meter records are itemized in your usage report. If you believe a charge is wrong, contact us within 30 days; we correct genuine metering errors with credit.

+

4. Acceptable use

+

You may not: (a) submit code you have no right to submit; (b) use the service to verify malware, weapons systems, or any unlawful purpose; (c) attempt to extract the CA signing keys, evade metering, or disrupt the service; (d) misrepresent a trial verdict as a certificate, or a revoked/expired certificate as valid.

+

5. Your responsibilities

+

You are responsible for the specifications you submit: the certificate binds the artifact hash, not your intent. The certificate credentials the code — it is our assessment that the submitted artifact was built to its specification, as mechanically checked under the stated toolchain. It does not state that your specification is correct, complete, safe, or fit for any purpose. We hold no responsibility beyond this assessment. Relying parties must read the Certificate Policy and validate every certificate through the published checker.

+

6. Certificates and reliance

+

Certificates credential the code submitted: our assessment that the artifact was built to its specification, as mechanically checked. They are factual statements about a verification event, valid for 90 days unless revoked earlier. We publish a revocation list and will revoke certificates affected by toolchain or engine defects. Certificates are not insurance, warranties, or guarantees of software behavior. We hold no responsibility beyond the assessment stated in the certificate.

+

7. Liability

+

To the maximum extent permitted by law: the service is provided “as is”; we disclaim implied warranties of merchantability and fitness for purpose. Our liability arising from any single certificate is limited to the fees paid for the verification that produced that certificate, and our aggregate liability for all claims is limited to the amount you paid us in the 12 months preceding the claim. We are not liable for indirect, incidental, or consequential damages, including losses from reliance on a certificate. We owe no duty to relying parties beyond the statements in the Certificate Policy; anyone who relies on a certificate does so at their own risk and must validate it through the published checker and revocation list before relying. These terms should be reviewed by qualified legal counsel; insurance backing the CA operation is part of our operating cost and is reflected in pricing.

+

8. Changes and termination

+

We may update these terms with 14 days’ notice on this page; continued use is acceptance. We may suspend accounts for abuse, non-payment, or unlawful use. You may stop using the service at any time; unused credits remain refundable per the Refund Policy.

+

9. Contact

+

Questions about these terms: hello@axiom-code.com.

+
+ + \ No newline at end of file diff --git a/site/dist/pricing/index.html b/site/dist/pricing/index.html new file mode 100644 index 0000000..0ca07e2 --- /dev/null +++ b/site/dist/pricing/index.html @@ -0,0 +1,252 @@ + + + + + +Pricing | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

Pricing

+

The trial proves the engine. The certificate is the product.

+
Our pricing covers the full cost of running the service — infrastructure, compute, operations, support, and insurance — plus a standard margin. One credit is always US$0.01. Verification consumes credits by compute time; the certificate itself is included with every paid verification.
+
+
+
+

Trial

$0
no card required
+
    +
  • 10 verifications
    • +
  • Full verdict + proof transcript
    • +
  • No certificates — trial verdicts are not certifiable
    • +
  • Rate-limited, fair use
    • +
+

Start verifying

+
+
+

Starter

$10
1,000 credits, never expire
+
    +
  • Roughly 30–100 typical verifications
    • +
  • Signed certificates on every pass
    • +
  • REST API + API key
    • +
  • Certificate checker + revocation list
    • +
+

+
+
+

Growth

$50
5,000 credits, never expire
+
    +
  • Roughly 150–500 typical verifications
    • +
  • Signed certificates on every pass
    • +
  • REST API + MCP server access
    • +
  • Usage reports & audit log
    • +
+

+
+
+

Scale

$200
20,000 credits, never expire
+
    +
  • Roughly 600–2,000 typical verifications
    • +
  • Signed certificates on every pass
    • +
  • Everything in Growth
    • +
  • Priority verification queue
    • +
+

+
+
+
+

How metering works

+

Each verification is metered by compute time at 0.9 credits/second (about $0.009/s). A small spec that checks in 12 seconds costs ~11 credits — eleven cents. You see the exact charge with every verdict, and your usage report itemizes all of it. Credits never expire. Unused credits are refundable within 14 days — see the Refund Policy.

+

Why the trial has no certificates

+

The trial exists so you can evaluate the engine: real verdicts, real transcripts, real evidence. But a certificate is a trust instrument — it says AxiomCode stakes its name on this verdict. We only stake our name in a commercial relationship, where the full cost of standing behind the verdict is covered. That boundary is what keeps the certificates meaningful.

+
+
What counts as a “typical verification”?

A Lean 4 spec that compiles and checks in 10–60 seconds of engine time. Very large developments cost proportionally more; the meter is compute time, so you always pay for what you used.

+
Do certificates really expire?

Yes — 90 days, like TLS. Software changes and toolchains move on; re-verification keeps the evidence fresh. Renewal pricing is the same credit meter.

+
What if a certificate was wrongly issued?

We revoke it publicly and say so. Mis-issuance handling is documented in the Certificate Policy — it’s the core of the trust model.

+
+
+
+ + + + + \ No newline at end of file diff --git a/site/dist/robots.txt b/site/dist/robots.txt new file mode 100644 index 0000000..c75cab2 --- /dev/null +++ b/site/dist/robots.txt @@ -0,0 +1,4 @@ +User-agent: * +Allow: / + +Sitemap: https://axiom-code.com/sitemap.xml diff --git a/site/dist/sitemap.xml b/site/dist/sitemap.xml new file mode 100644 index 0000000..6f9b5d8 --- /dev/null +++ b/site/dist/sitemap.xml @@ -0,0 +1,19 @@ + + + https://axiom-code.com/weekly + https://axiom-code.com/how-it-works/weekly + https://axiom-code.com/pricing/weekly + https://axiom-code.com/docs/weekly + https://axiom-code.com/docs/api/weekly + https://axiom-code.com/verify/weekly + https://axiom-code.com/check/weekly + https://axiom-code.com/paperwork/weekly + https://axiom-code.com/paperwork/terms/weekly + https://axiom-code.com/paperwork/privacy/weekly + https://axiom-code.com/paperwork/certificate-policy/weekly + https://axiom-code.com/paperwork/refunds/weekly + https://axiom-code.com/paperwork/sla/weekly + https://axiom-code.com/paperwork/security/weekly + https://axiom-code.com/blog/weekly + https://axiom-code.com/blog/dont-trust-our-ai/weekly + \ No newline at end of file diff --git a/site/dist/verify/index.html b/site/dist/verify/index.html new file mode 100644 index 0000000..aaa4196 --- /dev/null +++ b/site/dist/verify/index.html @@ -0,0 +1,182 @@ + + + + + +Verify — free trial | AxiomCode + + + + + + + + + + + + + + +
+AxiomCode + +Try free +
+
+

Verify — free trial

+

10 free verifications. Real verdicts, real transcripts. No certificates on trial — the certificate is the product, and it ships with paid verification.

+
The verification backend is being connected to this page as part of the launch rollout. If the button reports the API as unreachable, the engine isn’t wired yet — check back shortly or email hello@axiom-code.com.
+ + + + +

+
+

A PASSED trial verdict proves the engine works. To get the signed certificate — the thing you can hand to an auditor, a customer, or a counterparty — buy credits.

+
+ + + + \ No newline at end of file diff --git a/site/gen_docx.py b/site/gen_docx.py new file mode 100644 index 0000000..334ee6d --- /dev/null +++ b/site/gen_docx.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +"""Generate .docx versions of the paperwork pages (no banners, no tracked changes, no comments).""" + +import html as ihtml +import os +import re +import sys + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +from build import PAGES # noqa +import pages_paperwork # noqa: F401 (registers pages) +from docx import Document +from docx.shared import Pt, RGBColor + +INK = RGBColor(0x10, 0x18, 0x28) +GOLD = RGBColor(0xB9, 0x8A, 0x2F) +MUTED = RGBColor(0x47, 0x54, 0x67) + + +def clean_text(s): + s = re.sub(r"<[^>]+>", "", s) + return ihtml.unescape(s).strip() + + +def add_runs(para, html): + # minimal inline markup: , , , + tok = re.split(r"(.*?|.*?|.*?|.*?)", html) + for t in tok: + if not t: + continue + m = re.match(r"<(strong|em|code|a)(.*?)>(.*)$", t, re.S) + if not m: + para.add_run(ihtml.unescape(t)) + continue + tag, attrs, inner = m.groups() + text = ihtml.unescape(re.sub(r"<[^>]+>", "", inner)) + run = para.add_run(text) + if tag == "strong": + run.bold = True + elif tag == "em": + run.italic = True + elif tag == "code": + run.font.name = "Consolas" + run.font.size = Pt(10) + elif tag == "a": + href = re.search(r'href="([^"]+)"', attrs) + if href: + text = f"{text} ({href.group(1)})" + run.text = text + + +def body_to_docx(doc, body): + # strip section/wrap/prose scaffolding divs but keep their inner content + chunks = re.split( + r'(|

.*?

||
    .*?
|
]*>|

$", "", ch)) + for r in p.runs: + r.font.size = Pt(12) + r.font.color.rgb = MUTED + elif ch.startswith("]*>|

$", "", ch)) + elif ch.startswith("(.*?)", ch, re.S): + p = doc.add_paragraph(style="List Bullet") + add_runs(p, li) + elif 'class="note' in ch: + inner = re.sub(r"^]*>|
$", "", ch, flags=re.S) + p = doc.add_paragraph() + add_runs(p, inner) + for r in p.runs: + r.font.color.rgb = GOLD + r.bold = True + + +OUTDIR = os.path.join(os.path.dirname(os.path.abspath(__file__)), "paperwork-docx") +os.makedirs(OUTDIR, exist_ok=True) +made = [] +for path, title, _desc, body, _ in PAGES: + if not path.startswith("/paperwork/") or path == "/paperwork/": + continue + doc = Document() + st = doc.styles["Normal"] + st.font.name = "Calibri" + st.font.size = Pt(11) + t = doc.add_paragraph() + r = t.add_run(title) + r.bold = True + r.font.size = Pt(20) + r.font.color.rgb = INK + s = doc.add_paragraph() + r = s.add_run("AxiomCode \u2014 Last updated 26 September 2026") + r.font.size = Pt(10) + r.font.color.rgb = MUTED + body_to_docx(doc, body) + # hygiene: no tracked changes / comments / banners by construction; verify no DRAFT text + full = "\n".join(p.text for p in doc.paragraphs) + assert "DRAFT" not in full.upper() or "draft" in title.lower(), f"banner text in {title}" + assert len(doc.paragraphs) > 3, f"empty doc {title}" + fname = path.strip("/").replace("/", "-") + ".docx" + doc.save(os.path.join(OUTDIR, fname)) + made.append(fname) +print("wrote:", ", ".join(made)) diff --git a/site/pages_blog.py b/site/pages_blog.py new file mode 100644 index 0000000..383f1a0 --- /dev/null +++ b/site/pages_blog.py @@ -0,0 +1,110 @@ +from build import API_BASE, SITE, page + +# ---------- blog ---------- +page( + "/blog/", + "Blog", + "The AxiomCode blog: verification-as-evidence, certification practice, and honest notes on building a CA for software correctness.", + """
+

Blog

+

Notes on verification-as-evidence and building a certification authority for software.

+
+
26 September 2026
+

Don’t trust our AI — verify our proof

+

Why we built a certification authority for software correctness, why the trial gives you everything except the certificate, and why mis-issuance — saying “verified” when it isn’t — is the one risk we organize the whole company around.

+
+
+""", +) + +page( + "/blog/dont-trust-our-ai/", + "Don\u2019t trust our AI \u2014 verify our proof", + "Launch essay: why AxiomCode is a certification authority for software correctness, why verification-as-evidence beats verification-as-opinion, and why the certificate is never free.", + """
+
26 September 2026 · Launch
+

Don’t trust our AI — verify our proof

+

Why we built a certification authority for software correctness.

+ +

AI writes code now. A lot of it. And the industry’s answer to “is it right?” is still, essentially, vibes: code review (opinion), tests (samples), audits (expensive snapshots). All useful. None of them evidence.

+ +

We started AxiomCode with a different premise: correctness should be certifiable the way identity is. When you visit your bank, you don’t read the bank’s audit report — your browser checks a certificate issued by an authority whose entire business is not lying about identity. Software needs the same thing for correctness: a party whose business is not lying about verification.

+ +

Verification-as-evidence, not verification-as-opinion

+

An AI code reviewer gives you an opinion. AxiomCode gives you evidence: the artifact hash, the toolchain that ran, the transcript of the check, sealed under our signature. You don’t have to believe us — or our AI. Re-run the check yourself. The certificate tells you exactly what was verified and how.

+ +

The trial gives you everything except the certificate

+

Try us free: 10 verifications, real verdicts, real transcripts. But no certificates. That isn’t stinginess — it’s the business model working as designed. A certificate says we stake our name on this verdict. Staking our name costs real money: the compute, the operations, the insurance, the revocation infrastructure, the people who answer when something goes wrong. We only stake it inside a commercial relationship where those costs are covered. A free certificate would be a souvenir. Ours is a trust instrument.

+ +

The one risk we organize around

+

A certification authority has exactly one existential risk: mis-issuance — saying “verified” when it isn’t. Everything about the design flows from that: the engine rejects sorry, admit, vacuous builds, and broken proofs loudly. Certificates expire in 90 days so evidence stays fresh. And if our toolchain is ever wrong, we revoke publicly — there is no silent un-verification. Like TLS, but for correctness.

+ +

Who it’s for

+

Whoever has to prove correctness to a third party: regulated teams facing auditors, fintech and smart-contract builders moving money, agent builders whose agents ship code, procurement teams who want “certified correct” as a deliverable. If you’re that person, run your first verification free. Don’t trust our AI — verify our proof.

+
+""", + { + "@context": "https://schema.org", + "@type": "BlogPosting", + "headline": "Don\u2019t trust our AI \u2014 verify our proof", + "datePublished": "2026-09-26", + "author": {"@type": "Organization", "name": "AxiomCode"}, + }, +) + +# ---------- machine-readable extras (written by runner) ---------- +WELLKNOWN = { + "service": "AxiomCode", + "description": "Certification authority for software correctness. Machine-checked proofs, signed certificates.", + "homepage": SITE, + "api_base": API_BASE, + "mcp": API_BASE + "/mcp", + "llms_txt": SITE + "/llms.txt", + "docs": SITE + "/docs/api/", + "certificate_checker": SITE + "/check/", + "revocation_list": API_BASE + "/v1/revoked", + "ca_public_keys": SITE + "/.well-known/axiomcode-keys.json", + "pricing": SITE + "/pricing/", + "trial": {"verifications": 10, "certificates": False}, + "contact": "hello@axiom-code.com", +} + +LLMS_TXT = """# AxiomCode + +> The certification authority for software correctness. Don't trust our AI — verify our proof. + +AxiomCode verifies Lean 4 software specifications with a real toolchain and issues +signed, revocable, independently verifiable certificates binding the artifact hash, +verdict, toolchain, issuer, serial, and validity window. + +## For agents + +- API docs: https://axiom-code.com/docs/api/ +- Machine-readable service info: https://axiom-code.com/.well-known/axiomcode.json +- REST base: https://api.axiom-code.com +- MCP server: https://api.axiom-code.com/mcp with tools: verify, check_certificate, pricing, usage_report +- Check any certificate (no auth): GET https://api.axiom-code.com/v1/check?serial=... +- Revocation list: https://api.axiom-code.com/v1/revoked + +## Trial + +10 free verifications per email via POST /v1/trial/verify. Trial verdicts include the +verdict and transcript but NEVER a certificate. Certificates are issued to paying +customers only (credit packs from $10; 1 credit = $0.01; metered at 0.9 credits/sec +of engine compute time). + +## Scope (honest) + +Today: Lean 4 only. A PASSED verdict means the submitted artifact compiled under the +stated toolchain and its proofs checked. It does not certify intent, deployment, or +the rest of the system. Certificates are valid 90 days and revocable. Mis-issuance +is handled by public revocation — see the Certificate Policy. + +## Paperwork + +- Terms: https://axiom-code.com/paperwork/terms/ +- Privacy: https://axiom-code.com/paperwork/privacy/ +- Certificate Policy & CPS: https://axiom-code.com/paperwork/certificate-policy/ +- Refunds: https://axiom-code.com/paperwork/refunds/ +- Security & disclosure: https://axiom-code.com/paperwork/security/ +""" diff --git a/site/pages_docs.py b/site/pages_docs.py new file mode 100644 index 0000000..592168d --- /dev/null +++ b/site/pages_docs.py @@ -0,0 +1,217 @@ +import json + +from build import API_BASE, page + +# ---------- docs (humans) ---------- +page( + "/docs/", + "Documentation", + "AxiomCode documentation for humans: writing verifiable Lean 4 specifications, reading verdicts and certificates, and understanding verification scope.", + """
+

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

+ + + + + +
VerdictMeaningCertificate?
PASSEDThe toolchain compiled the artifact and the proof checked.Yes (paid only)
FAILEDThe proof does not check. The transcript shows why.No
INCOMPLETEDoesn’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 certificate credentials the code — our assessment that the submitted artifact was built to its specification, as mechanically checked. We hold no responsibility beyond this assessment. 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.
    • +
+
+""", +) + +# ---------- docs/api (agents) ---------- +page( + "/docs/api/", + "REST & MCP API", + "AxiomCode API for applications and AI agents: REST endpoints, MCP tools, authentication, metering, and machine-readable discovery.", + """
+

REST & MCP API

+

Built for agents first. Humans welcome.

+
Machine-readable:  llms.txt · /.well-known/axiomcode.json · OpenAPI (JSON)
+ +

Base URL

+

https://api.axiom-code.com

+ +

Authentication

+

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.

+ +

REST endpoints

+ + + + + + + +
Method & pathAuthWhat it does
POST /v1/trial/verifyemailVerify a Lean artifact. Returns verdict + transcript. No certificate. 10 lifetime uses per email.
POST /v1/verifyAPI keyVerify and, on pass, issue a signed certificate. Metered by compute time.
GET /v1/check?serial=...noneCertificate status: VALID / REVOKED / EXPIRED, with reason.
GET /v1/revokednoneThe public revocation list.
GET /v1/accountAPI keyCredit balance and usage report.
+ +

Example: trial verification

+
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."}
+ +

MCP server

+

Endpoint: https://api.axiom-code.com/mcp (streamable HTTP). Tools:

+ + + + + + +
ToolWhat it does
verifySubmit a Lean artifact; returns verdict, transcript, and (paid) certificate.
check_certificateValidate a certificate by serial.
pricingCurrent credit price and pack list.
usage_reportMetered usage for your API key.
+
Agent pattern: after your coding agent finishes a safety-critical function, have it write the Lean spec and call verify. Ship the certificate with the code — your user can check it without trusting your agent.
+ +

Metering

+

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.

+ +

Rate limits & abuse

+
    +
  • Trial: 10 verifications per email, lifetime; 1 concurrent request.
    • +
  • Paid: 5 concurrent verifications per key by default; contact us for more.
    • +
  • Submissions are capped at 2 MB of source; engine time is capped per call.
    • +
  • We may suspend keys used to probe the engine adversarially or to resell trial access. See the Terms.
    • +
+
+""", +) + +# ---------- verify (trial UI) ---------- +page( + "/verify/", + "Verify \u2014 free trial", + "Try AxiomCode free: submit a Lean 4 specification, get a real machine-checked verdict and proof transcript. 10 free verifications; trial verdicts carry no certificate.", + """
+

Verify — free trial

+

10 free verifications. Real verdicts, real transcripts. No certificates on trial — the certificate is the product, and it ships with paid verification.

+
The verification backend is being connected to this page as part of the launch rollout. If the button reports the API as unreachable, the engine isn’t wired yet — check back shortly or email hello@axiom-code.com.
+ + + + +

+
+

A PASSED trial verdict proves the engine works. To get the signed certificate — the thing you can hand to an auditor, a customer, or a counterparty — buy credits.

+
+ +""", +) + +# ---------- check (cert validation UI) ---------- +page( + "/check/", + "Check a certificate", + "Validate an AxiomCode certificate: paste the certificate JSON and get VALID, REVOKED, or EXPIRED with the reason. No account needed.", + """
+

Check a certificate

+

No account needed. Paste the certificate JSON — we’ll tell you if it’s VALID, REVOKED, or EXPIRED, and why.

+ + +

+
+
Don’t trust our AI — verify our proof. A certificate is only as good as its checkability. This page, the API, and the published revocation list are how you hold us accountable.
+
+ +""", +) diff --git a/site/pages_main.py b/site/pages_main.py new file mode 100644 index 0000000..501b462 --- /dev/null +++ b/site/pages_main.py @@ -0,0 +1,246 @@ +import json + +from build import HERO_LINE, PADDLE_VENDOR, PRICE_IDS, SITE, TAGLINE, page + +# ---------- landing ---------- +ORG_JSONLD = { + "@context": "https://schema.org", + "@type": "Organization", + "name": "AxiomCode", + "url": SITE, + "description": "The certification authority for software correctness. Machine-checked proofs, signed certificates, independently verifiable.", + "email": "hello@axiom-code.com", +} + +page( + "/", + "Software correctness, certified", + "AxiomCode is the certification authority for software correctness. Submit a specification, get a machine-checked proof and a signed certificate anyone can verify.", + f"""
+

{HERO_LINE}

+

{TAGLINE} Submit your specification. Our engine compiles it, checks the proof mechanically, and issues a signed certificate — binding your code hash, the verification result, and our identity — that anyone can re-check without trusting us.

+
+Verify something free +How it works +
+

10 free trial verifications · no certificate until you pay · certificates valid 90 days, revocable, publicly checkable

+
+ +
+
The problem
+

AI writes code. Nobody can prove it’s right.

+

Code review is opinion. Tests are samples. Audits are expensive snapshots. When software has to be right — money movement, access control, safety logic, smart contracts — “looks good to me” is not evidence. AxiomCode sells verification-as-evidence: a mechanical proof, checked by a real toolchain, sealed into a certificate you can hand to a regulator, a customer, or a counterparty.

+
+
+
1

Submit

Send a Lean 4 specification through the web UI, the REST API, or the MCP server — the way your agent already talks to tools.

+
2

We check it mechanically

The engine compiles your spec with the real Lean toolchain and checks the proof. Vacuous builds, sorry, admit, and broken proofs are rejected — loudly.

+
3

You get a certificate

A signed certificate binding your artifact hash, the verdict, the toolchain, the issuer, and a validity window. Anyone can re-verify it without trusting us.

+
+
+ +
+
The guarantee
+

Our honesty is structural, not promised.

+

A certificate authority lives or dies on one thing: never saying “verified” when it isn’t. So we built the incentives into the system:

+
+
+

Mis-issuance is the existential risk

Every certificate carries a serial number, issuer identity, and validity window. If our toolchain is ever wrong, we revoke — publicly, through a published revocation list. Like TLS, but for correctness.

+

Expiry drives re-verification

Certificates last 90 days. Software changes; proofs should be re-run. Renewal is the business model, the same way TLS renewal is.

+

You don’t have to trust us

The certificate binds the artifact hash and the proof transcript. Re-run the check yourself with the published toolchain. “Don’t trust our AI — verify our proof” isn’t a slogan; it’s the architecture.

+
+
+ +
+
Who it’s for
+

Whoever has to prove it’s correct.

+

The buyer isn’t whoever writes the code. It’s whoever must demonstrate correctness to a third party:

+
    +
  • Regulated software teams — hand a certificate to the auditor instead of a test report.
    • +
  • Fintech & smart contracts — money logic with a machine-checked proof attached.
    • +
  • AI agent builders — agents that ship code can now ship the proof too. Call us from your agent over MCP.
    • +
  • Procurement & contracts — “certified correct” as a deliverable, checkable by the buyer.
    • +
+

See pricing

+
+ +
+
Honest scope
+

What we certify today — and what we don’t.

+

Today the engine verifies Lean 4 specifications. The certificate credentials the code: it is our assessment that the submitted artifact was built to its specification, as mechanically checked — recorded as the artifact hash, the toolchain version, and the verdict. We hold no responsibility beyond this assessment. We do not claim your whole system is correct, your spec matches your intent, or your deployment matches the artifact. Read the Certificate Policy for the precise meaning of every field.

+
Verification is evidence, not opinion. The evidence is bounded, and we publish the bounds.
+
+""", + ORG_JSONLD, +) + +# ---------- how it works ---------- +page( + "/how-it-works/", + "How it works", + "How AxiomCode verification works: submit a Lean 4 specification, the engine compiles and checks the proof, and you receive a signed, revocable, independently verifiable certificate.", + """
+

How it works

+

Three steps. Every one of them checkable.

+ +

1. Submit the artifact

+

Paste Lean 4 code into the web verifier, POST it to the REST API, or call the verify tool on our MCP server. What you submit is hashed (SHA-256) the moment it arrives — that hash becomes part of the certificate, so the verdict can never drift away from the code it describes.

+ +

2. The engine checks the proof — for real

+

The verification engine runs the actual Lean toolchain (lake build) against your artifact in an isolated project. It is deliberately adversarial toward sloppy proofs:

+
    +
  • Vacuous builds rejected. A target that compiles nothing is not a proof of anything.
    • +
  • sorry and admit rejected. Placeholders are not proofs.
    • +
  • Broken proofs rejected. If the toolchain reports an error, the verdict is FAILED, with the log attached.
    • +
  • Unfinished work reported honestly. Something that doesn’t compile yet gets INCOMPLETE — never a pass.
    • +
+

A pass means one thing: the toolchain compiled your artifact and the proof checked. The full transcript ships with the verdict.

+ +

3. The certificate seals the evidence

+

On PASSED, the certification authority issues a signed certificate. The certificate credentials the code — our assessment that the artifact was built to its specification, as mechanically checked — and we hold no responsibility beyond this assessment. It contains:

+ + + + + + + + + +
FieldMeaning
artifact_sha256Hash of exactly the code that was checked
verdictPASSED, with the toolchain transcript reference
toolchainLean / lake versions that ran the check
issuerAxiomCode CA
serialUnique serial number
validity90-day window (notBefore / notAfter)
signatureCA signature over all of the above
+
+

Check any certificate, no account needed: paste it into the certificate checker. You’ll get VALID, REVOKED, or EXPIRED — with the reason. Revocation is published, not hidden: if a toolchain bug ever invalidates a verdict, the serial goes on the public revocation list.

+
+ +

Interfaces

+ +
+""", +) + +# ---------- pricing ---------- +PRODUCT_JSONLD = { + "@context": "https://schema.org", + "@type": "Product", + "name": "AxiomCode verification credits", + "description": "Credits for machine-checked software verification with signed certificates. 1 credit = US$0.01.", + "brand": {"@type": "Brand", "name": "AxiomCode"}, + "offers": [ + { + "@type": "Offer", + "name": "Trial", + "price": "0", + "priceCurrency": "USD", + "description": "10 free verifications. Verdicts only, no certificates.", + }, + { + "@type": "Offer", + "name": "Starter", + "price": "10", + "priceCurrency": "USD", + "description": "1,000 credits. Certificates included.", + }, + { + "@type": "Offer", + "name": "Growth", + "price": "50", + "priceCurrency": "USD", + "description": "5,000 credits. Certificates included.", + }, + { + "@type": "Offer", + "name": "Scale", + "price": "200", + "priceCurrency": "USD", + "description": "20,000 credits. Certificates included.", + }, + ], +} + +page( + "/pricing/", + "Pricing", + "AxiomCode pricing: 10 free trial verifications (no certificates), then credit packs. 1 credit = $0.01. Certificates are issued to paying customers only.", + """
+

Pricing

+

The trial proves the engine. The certificate is the product.

+
Our pricing covers the full cost of running the service — infrastructure, compute, operations, support, and insurance — plus a standard margin. One credit is always US$0.01. Verification consumes credits by compute time; the certificate itself is included with every paid verification.
+
+
+
+

Trial

$0
no card required
+
    +
  • 10 verifications
    • +
  • Full verdict + proof transcript
    • +
  • No certificates — trial verdicts are not certifiable
    • +
  • Rate-limited, fair use
    • +
+

Start verifying

+
+
+

Starter

$10
1,000 credits, never expire
+
    +
  • Roughly 30–100 typical verifications
    • +
  • Signed certificates on every pass
    • +
  • REST API + API key
    • +
  • Certificate checker + revocation list
    • +
+

+
+
+

Growth

$50
5,000 credits, never expire
+
    +
  • Roughly 150–500 typical verifications
    • +
  • Signed certificates on every pass
    • +
  • REST API + MCP server access
    • +
  • Usage reports & audit log
    • +
+

+
+
+

Scale

$200
20,000 credits, never expire
+
    +
  • Roughly 600–2,000 typical verifications
    • +
  • Signed certificates on every pass
    • +
  • Everything in Growth
    • +
  • Priority verification queue
    • +
+

+
+
+
+

How metering works

+

Each verification is metered by compute time at 0.9 credits/second (about $0.009/s). A small spec that checks in 12 seconds costs ~11 credits — eleven cents. You see the exact charge with every verdict, and your usage report itemizes all of it. Credits never expire. Unused credits are refundable within 14 days — see the Refund Policy.

+

Why the trial has no certificates

+

The trial exists so you can evaluate the engine: real verdicts, real transcripts, real evidence. But a certificate is a trust instrument — it says AxiomCode stakes its name on this verdict. We only stake our name in a commercial relationship, where the full cost of standing behind the verdict is covered. That boundary is what keeps the certificates meaningful.

+
+
What counts as a “typical verification”?

A Lean 4 spec that compiles and checks in 10–60 seconds of engine time. Very large developments cost proportionally more; the meter is compute time, so you always pay for what you used.

+
Do certificates really expire?

Yes — 90 days, like TLS. Software changes and toolchains move on; re-verification keeps the evidence fresh. Renewal pricing is the same credit meter.

+
What if a certificate was wrongly issued?

We revoke it publicly and say so. Mis-issuance handling is documented in the Certificate Policy — it’s the core of the trust model.

+
+
+
+ + +""", + PRODUCT_JSONLD, +) diff --git a/site/pages_paperwork.py b/site/pages_paperwork.py new file mode 100644 index 0000000..1fbb7fc --- /dev/null +++ b/site/pages_paperwork.py @@ -0,0 +1,186 @@ +from build import page + +# ---------- paperwork ---------- +PW_INTRO = """
+
These documents govern the AxiomCode service. They are written in plain language and describe process and outcomes, not marketing claims. Material liability and warranty terms should be reviewed by qualified legal counsel before they are relied upon in any dispute.
+""" + + +def pw_page(path, title, desc, body): + slug = path.strip("/").replace("/", "-") if path != "/paperwork/" else "" + dl = f'

Download as Word (.docx)

' if slug else "" + page( + path, + title, + desc, + PW_INTRO + + f'

{title}

Last updated: 26 September 2026

' + + dl + + body + + "
", + ) + + +pw_page( + "/paperwork/", + "Trust & paperwork", + "AxiomCode trust centre: Terms of Service, Privacy Policy, Certificate Policy and CPS, Refund Policy, Service Levels, and Security.", + """

Everything that governs the service, in one place.

+ +

Downloadable Word copies of each document are linked at the top of each page.

+""", +) + +pw_page( + "/paperwork/terms/", + "Terms of Service", + "AxiomCode Terms of Service: the service, trial terms, credits and payment, acceptable use, certificate reliance, liability limits.", + """

1. The service

+

AxiomCode (“we”) provides machine-checked verification of software specifications and issues signed certificates recording the verification outcome (“certificates”). The service is offered through a web interface, a REST API, and an MCP server.

+

2. Trial

+

New users may run up to 10 trial verifications without payment. Trial verdicts include the verdict and the engine transcript; trial verdicts never include certificates. Trial access is rate-limited and may not be resold, shared across accounts to evade the limit, or used to probe the engine adversarially.

+

3. Credits and payment

+

Paid verification consumes credits (1 credit = US$0.01), metered by engine compute time at the published rate. Credits are purchased in packs through our merchant of record and never expire. Meter records are itemized in your usage report. If you believe a charge is wrong, contact us within 30 days; we correct genuine metering errors with credit.

+

4. Acceptable use

+

You may not: (a) submit code you have no right to submit; (b) use the service to verify malware, weapons systems, or any unlawful purpose; (c) attempt to extract the CA signing keys, evade metering, or disrupt the service; (d) misrepresent a trial verdict as a certificate, or a revoked/expired certificate as valid.

+

5. Your responsibilities

+

You are responsible for the specifications you submit: the certificate binds the artifact hash, not your intent. The certificate credentials the code — it is our assessment that the submitted artifact was built to its specification, as mechanically checked under the stated toolchain. It does not state that your specification is correct, complete, safe, or fit for any purpose. We hold no responsibility beyond this assessment. Relying parties must read the Certificate Policy and validate every certificate through the published checker.

+

6. Certificates and reliance

+

Certificates credential the code submitted: our assessment that the artifact was built to its specification, as mechanically checked. They are factual statements about a verification event, valid for 90 days unless revoked earlier. We publish a revocation list and will revoke certificates affected by toolchain or engine defects. Certificates are not insurance, warranties, or guarantees of software behavior. We hold no responsibility beyond the assessment stated in the certificate.

+

7. Liability

+

To the maximum extent permitted by law: the service is provided “as is”; we disclaim implied warranties of merchantability and fitness for purpose. Our liability arising from any single certificate is limited to the fees paid for the verification that produced that certificate, and our aggregate liability for all claims is limited to the amount you paid us in the 12 months preceding the claim. We are not liable for indirect, incidental, or consequential damages, including losses from reliance on a certificate. We owe no duty to relying parties beyond the statements in the Certificate Policy; anyone who relies on a certificate does so at their own risk and must validate it through the published checker and revocation list before relying. These terms should be reviewed by qualified legal counsel; insurance backing the CA operation is part of our operating cost and is reflected in pricing.

+

8. Changes and termination

+

We may update these terms with 14 days’ notice on this page; continued use is acceptance. We may suspend accounts for abuse, non-payment, or unlawful use. You may stop using the service at any time; unused credits remain refundable per the Refund Policy.

+

9. Contact

+

Questions about these terms: hello@axiom-code.com.

+""", +) + +pw_page( + "/paperwork/privacy/", + "Privacy Policy", + "AxiomCode Privacy Policy: what data we collect (submitted code, account, metering), why we keep it, retention and deletion, and our no-sale commitment.", + """

1. What we collect

+
    +
  • Submitted artifacts: the code you ask us to verify, its SHA-256 hash, the verdict, and the engine transcript. We cannot verify without it.
    • +
  • Account data: email address, API keys, credit balance, and purchase records from our merchant of record.
    • +
  • Metering records: compute time, credits charged, timestamps — kept in a tamper-evident log so your bill always reconciles.
    • +
  • Operational logs: IP addresses and request metadata for abuse prevention, kept briefly.
    • +
+

2. What we never do

+

We never sell your data. We never use your submitted code to train models. We never disclose your artifacts except as needed to operate the service (e.g., payment processing by our merchant of record) or as required by law.

+

3. Why certificates are public-ish

+

A certificate is useful precisely because third parties can check it. Certificate contents (artifact hash, verdict, toolchain, serial, validity) and the revocation list are queryable by anyone. The artifact source itself is not published — only its hash.

+

4. Retention and deletion

+
    +
  • Artifacts and transcripts: retained while your account is active, to support re-verification and dispute handling; deleted within 90 days of account closure on request.
    • +
  • Metering and purchase records: retained as required for tax and accounting (typically 7 years), in anonymized form where possible after closure.
    • +
  • Operational logs: 30 days.
    • +
+

To request deletion or a copy of your data: hello@axiom-code.com. Some records (revoked certificate entries, tax records) cannot be deleted while the law requires them.

+

5. Security

+

CA signing keys are held separately from the web service with restricted access; see Security. No method is perfect; we disclose breaches affecting your data promptly.

+""", +) + +pw_page( + "/paperwork/certificate-policy/", + "Certificate Policy & Certification Practice Statement", + "AxiomCode Certificate Policy and CPS: what certificates assert, validation method, issuance, 90-day validity, renewal, revocation, and incident handling.", + """

This document follows the structure of RFC 3647. It states what AxiomCode certificates mean, how they are issued, and what happens when something goes wrong. It should be reviewed by qualified legal counsel and a PKI auditor before certificates are relied upon in regulated contexts.

+

1. Introduction

+

1.1 Overview. AxiomCode operates a certification authority (“AxiomCode CA”) that issues certificates binding a software artifact’s hash to a machine-checked verification verdict. Verification-as-evidence, not verification-as-opinion: every certificate carries the evidence needed to re-check it.

+

1.2 Document name. AxiomCode Certificate Policy and Certification Practice Statement, version 1.0 (2026-09-26).

+

1.3 Participants. The CA (AxiomCode), subscribers (paying customers who request verification), and relying parties (anyone who validates a certificate).

+

1.4 Certificate usage. Each certificate credentials the code submitted: it is our assessment that the artifact with the stated hash was built to its specification, as mechanically checked by the stated toolchain on the stated date. We hold no responsibility beyond this assessment. Appropriate uses: audit evidence, procurement deliverables, counterparty assurance. Prohibited reliance: treating a certificate as a warranty of safety, fitness, or intent — see §9.

+

2. Publication

+

The CP/CPS, the CA’s public verification keys, and the revocation list are published at axiom-code.com and queryable without an account.

+

3. Identification and authentication

+

Subscribers are identified by account (email + API key). Artifacts are identified by SHA-256 hash computed at submission. No identity vetting of persons is performed: the certificate speaks about the artifact, not the author.

+

4. Certificate life-cycle

+

4.1 Application. A paid verification request is a certificate application. Trial requests are never applications — no certificate can result.

+

4.2 Issuance. On a PASSED verdict, the CA signs a certificate containing artifact hash, verdict, toolchain versions, issuer name, unique serial, and a 90-day validity window. FAILED and INCOMPLETE verdicts produce no certificate, ever.

+

4.3 Validity and renewal. 90 days from issuance. Renewal is re-verification at the standard credit meter — there is no shortcut renewal, because the point is fresh evidence.

+

4.4 Revocation. The CA revokes a certificate when: (a) a toolchain or engine defect undermines the verdict; (b) the certificate was mis-issued; (c) the subscriber requests it. Revocations are published to the revocation list promptly (target: within 24 hours of the decision) and are permanent.

+

4.5 Incident handling. Suspected mis-issuance triggers an internal review; confirmed mis-issuance triggers revocation, a public incident note, and re-verification of affected artifacts at our expense. Mis-issuance is treated as the CA’s existential risk.

+

5. Operational controls

+

Verification runs in isolated, single-use build environments. CA signing keys are segregated from the web/API tier; signing requires the isolated CA service. All issuance, revocation, and metering events are written to a tamper-evident append-only log.

+

6. Technical security controls

+

Certificates are signed with modern asymmetric signatures (Ed25519); the CA’s public keys are published for independent verification. Key generation uses a vetted CSPRNG; private keys are access-controlled and backed up encrypted. Key compromise triggers key rollover, re-issuance of affected certificates, and public disclosure.

+

7. Certificate and revocation profiles

+

Certificates are signed JSON documents with the fields listed in How it works §3. The revocation list is a signed JSON document listing revoked serials with reason codes and timestamps, updated on every revocation.

+

8. Compliance

+

We log every issuance and revocation; logs are available to auditors under NDA. Annual self-assessment against this CP/CPS is published in summary form.

+

9. Legal matters

+

Certificates credential the code submitted and nothing more; they are factual statements about a verification event, not warranties. We hold no responsibility beyond the assessment stated in the certificate. Liability is limited as stated in the Terms of Service (per-certificate cap at the verification fee; aggregate cap at 12 months’ fees; no consequential damages; no duty to relying parties beyond this Policy). Subscribers warrant they have the right to submit the artifact. Relying parties must validate certificates through the published checker and revocation list before relying; any reliance is at the relying party’s own risk.

+""", +) + +pw_page( + "/paperwork/refunds/", + "Billing, trial & refund policy", + "AxiomCode billing policy: the 10-verification trial, credit packs, how metering works, cancellations, and the 14-day refund rule for unused credits.", + """

1. Trial

+

Every new email address gets 10 free verifications. Trial verdicts include the verdict and transcript but never a certificate. The trial demonstrates the engine; certification is the paid product. One trial per person; creating multiple accounts to harvest trials is abuse and will be suspended.

+

2. Credits

+
    +
  • 1 credit = US$0.01. Packs: Starter $10 (1,000 credits), Growth $50 (5,000), Scale $200 (20,000).
    • +
  • Verification consumes credits by engine compute time at 0.9 credits/second, shown with every verdict and itemized in your usage report.
    • +
  • Credits never expire and are not transferable between accounts.
    • +
  • Payment is processed by our merchant of record (Paddle); we never see or store your card.
    • +
+

3. Refunds

+

Unused credits are refundable within 14 days of purchase — email hello@axiom-code.com and we return the unused portion to the original payment method. Credits already consumed by verifications are not refundable: the compute was spent and the evidence delivered. Genuine metering errors are always corrected with credit, no time limit.

+

4. Cancellation

+

There are no subscriptions to cancel — credits are prepaid. Stop buying packs whenever you like; your balance, certificates, and history remain available.

+

5. Disputes

+

Dispute a charge within 30 days with the serial numbers or timestamps involved; we investigate against the tamper-evident meter log, which is the record of truth both sides can inspect.

+""", +) + +pw_page( + "/paperwork/sla/", + "Service levels & support", + "AxiomCode service levels: uptime target, verification queue expectations, support channels and response targets, and what happens when we miss.", + """

1. Uptime

+

Target: 99% monthly availability for the API and certificate checker, excluding scheduled maintenance (announced 48h ahead) and upstream outages. The static site and published revocation list are served from the edge and targeted higher, but the commitment we make is 99% on the API.

+

2. Verification queue

+

Verifications normally start within 60 seconds. At high load, paid verifications queue ahead of trial verifications, and Scale customers queue ahead of others. Engine time per call is capped; very large artifacts may be asked to split submissions.

+

3. Support

+
    +
  • Email: hello@axiom-code.com — target first response 1 business day.
    • +
  • Mis-issuance / revocation issues: treated as critical; target acknowledgment 4 business hours.
    • +
  • Docs and status: this site’s documentation; a status page ships with the production rollout.
    • +
+

4. Remedies

+

If monthly API availability falls below 99%, affected paying customers receive a 10% credit rebate for the month, applied automatically. This is our sole remedy for downtime and is without prejudice to the liability limits in the Terms.

+""", +) + +pw_page( + "/paperwork/security/", + "Security & responsible disclosure", + "AxiomCode security: how the CA and signing keys are protected, what we ask of researchers, and how to report vulnerabilities.", + """

1. How we protect the CA

+
    +
  • Key segregation: CA signing keys live in an isolated service, separate from the web and API tiers. The public internet never touches the signer.
    • +
  • Least privilege: few humans can touch the CA; every touch is logged.
    • +
  • Tamper-evident logs: issuance, revocation, and metering are append-only and hash-chained. If the log doesn’t reconcile, we treat it as an incident.
    • +
  • Isolated builds: every verification runs in a single-use environment; artifacts can’t see each other or the host.
    • +
  • Dependency hygiene: the Lean toolchain is pinned; upgrades are tested against the regression suite before they touch production verdicts.
    • +
+

2. Responsible disclosure

+

Found a vulnerability? Email security@axiom-code.com with the details and a way to reach you. We ask for a reasonable window (90 days) before public disclosure so we can fix, revoke affected certificates if needed, and publish an incident note. We commit to acknowledging within 2 business days and keeping you updated.

+

3. Scope

+

In scope: the API, the MCP server, the certificate checker, the CA issuance path, and this site. Out of scope: third-party services (Paddle, Cloudflare), social engineering, and physical attacks. Please don’t disrupt the service or access other customers’ data while researching.

+

4. What we won’t do

+

We won’t threaten researchers who follow this policy, and we won’t ask law enforcement to chill good-faith research. If you’re unsure whether something is in scope, ask first.

+""", +) diff --git a/site/paperwork-docx/paperwork-certificate-policy.docx b/site/paperwork-docx/paperwork-certificate-policy.docx new file mode 100644 index 0000000..e6e76dd Binary files /dev/null and b/site/paperwork-docx/paperwork-certificate-policy.docx differ diff --git a/site/paperwork-docx/paperwork-privacy.docx b/site/paperwork-docx/paperwork-privacy.docx new file mode 100644 index 0000000..fbcb24b Binary files /dev/null and b/site/paperwork-docx/paperwork-privacy.docx differ diff --git a/site/paperwork-docx/paperwork-refunds.docx b/site/paperwork-docx/paperwork-refunds.docx new file mode 100644 index 0000000..855bc5a Binary files /dev/null and b/site/paperwork-docx/paperwork-refunds.docx differ diff --git a/site/paperwork-docx/paperwork-security.docx b/site/paperwork-docx/paperwork-security.docx new file mode 100644 index 0000000..2f9001e Binary files /dev/null and b/site/paperwork-docx/paperwork-security.docx differ diff --git a/site/paperwork-docx/paperwork-sla.docx b/site/paperwork-docx/paperwork-sla.docx new file mode 100644 index 0000000..e2dc4e0 Binary files /dev/null and b/site/paperwork-docx/paperwork-sla.docx differ diff --git a/site/paperwork-docx/paperwork-terms.docx b/site/paperwork-docx/paperwork-terms.docx new file mode 100644 index 0000000..4c6c0d8 Binary files /dev/null and b/site/paperwork-docx/paperwork-terms.docx differ diff --git a/site/run.py b/site/run.py new file mode 100644 index 0000000..d9d873d --- /dev/null +++ b/site/run.py @@ -0,0 +1,54 @@ +#!/usr/bin/env python3 +"""Runner: import all page modules, render, write extras.""" + +import json +import os +import shutil +import sys + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +# import order is page registration order (drives sitemap.xml) - not alphabetical +import pages_main # noqa: F401, I001 (registration side effects) +import pages_docs # noqa: F401, I001 (registration side effects) +import pages_paperwork # noqa: F401, I001 (registration side effects) +import pages_blog +from build import API_BASE, render_all + +OUT = os.path.join(os.path.dirname(os.path.abspath(__file__)), "dist") +render_all(OUT) + +# machine-readable extras +wk = os.path.join(OUT, ".well-known") +os.makedirs(wk, exist_ok=True) +with open(os.path.join(wk, "axiomcode.json"), "w") as f: + json.dump(pages_blog.WELLKNOWN, f, indent=2) +with open(os.path.join(OUT, "llms.txt"), "w") as f: + f.write(pages_blog.LLMS_TXT) + +# stub OpenAPI for agents (full spec ships with the API) +openapi = { + "openapi": "3.0.3", + "info": { + "title": "AxiomCode API", + "version": "1.0.0", + "description": ("Verification and certification API. Full reference at https://axiom-code.com/docs/api/"), + }, + "servers": [{"url": API_BASE}], + "paths": { + "/v1/trial/verify": {"post": {"summary": "Trial verification (email, 10 lifetime, no certificate)"}}, + "/v1/verify": {"post": {"summary": "Paid verification with certificate (API key)"}}, + "/v1/check": {"get": {"summary": "Certificate status by serial (no auth)"}}, + "/v1/revoked": {"get": {"summary": "Public revocation list (no auth)"}}, + "/v1/account": {"get": {"summary": "Balance and usage (API key)"}}, + }, +} +api_dir = os.path.join(OUT, "docs", "api") +with open(os.path.join(api_dir, "openapi.json"), "w") as f: + json.dump(openapi, f, indent=2) + +# copy paperwork docx into dist +_src = os.path.join(os.path.dirname(os.path.abspath(__file__)), "paperwork-docx") +for _f in os.listdir(_src): + if _f.endswith(".docx"): + shutil.copy(os.path.join(_src, _f), os.path.join(OUT, "paperwork", _f)) +print("extras written") diff --git a/tests/test_llm_prover.py b/tests/test_llm_prover.py index afe5a69..0aa1f6c 100644 --- a/tests/test_llm_prover.py +++ b/tests/test_llm_prover.py @@ -222,7 +222,7 @@ def test_broken_code_not_verified(self, tmp_path): pytest.skip("lake not on PATH") proj = self._scratch_project(tmp_path) - src = proj / "E2E.lean" + src: Path = proj / "E2E.lean" def writer(code: str) -> Path: src.write_text(code) @@ -249,7 +249,7 @@ def test_good_code_verified(self, tmp_path): pytest.skip("lake not on PATH") proj = self._scratch_project(tmp_path) - src = proj / "E2E.lean" + src: Path = proj / "E2E.lean" def writer(code: str) -> Path: src.write_text(code)