athanor-sdk 0.4.9

Formal verification as agentic training signal — CLI + self-hosted runner

kairos

_{The SDK from Athanor AI. Distributed as athanor-kairos on PyPI; imports as kairos.}

Prove properties of your code in plain English.
Free tier: zero phone-home, no license required, Lean stays hidden.
Paid tier: full RTL verification stack + LLM-orchestrated multi-tier reasoning.

athanor-ai.com

---

Free tier in 30 seconds

pip install athanor-kairos
python -m kairos doctor          # preflight check (always run first)

from kairos import simple_prove_template

result = simple_prove_template("prove c_vector_sharp is positive")
print(result.summary)
# → ✓ proved. c_vector_sharp is strictly positive (Pythia.MatchingConstants).

That's the whole onboarding. No license, no API key, no Lean files written by hand. The SDK matches your hypothesis against built-in Pythia templates and runs Lean verification under the hood.

For hypotheses outside the built-in templates, bring your own LLM key (Anthropic / OpenAI / Gemini). the SDK never sees the key, calls go directly customer→provider.

Or scaffold a Lean project with Pythia + Mathlib + lean-machines pre-wired:

kairos init --lean-pythia --dest my-project
cd my-project && lake build && lake env lean Examples/Smoke.lean

→ Full free-tier guide: docs/free-tier-quickstart.md → Doc map: docs/INDEX.md

---

What kairos does

You have domain expertise. You know what correct code looks like. You want an AI agent (or a human engineer) to produce verified solutions, not guesses. kairos is the SDK that turns formal proofs into a usable contract.

Three layers, each one optional:

1. Free tier. kairos.simple_prove_template(...). Plain-English claims about Pythia specs. Zero setup beyond pip install. No license required.
2. 🔒 Paid tier. kairos.prove(...) and kairos.fleet.Orchestrator. Full LLM-orchestrated multi-tier reasoning across our supported verticals (RTL/SystemVerilog, Lean spec, hardware/software co-design). Requires a license file from Athanor.
3. Building blocks. kairos.verify_proof, kairos.lean_machines.*, kairos.sv.*. The lower-level primitives the higher-tier APIs are built on. Use directly if you already speak Lean / SVA.

---

Free-tier surface

Function	What it does	Phone-home?
simple_prove_template(hypothesis)	NL → Pythia template → Lean → verdict → NL. Hides Lean.	No
simple_prove(hypothesis, target_file)	Single-LLM proof against an existing Lean target file.	No
verify_proof(proof_code)	Run a Lean 4 proof through the compiler.	No
score_proof(proof_code)	Score a proof: 1.0 (full) / 0.35 (sorry) / 0.25 (broken) / 0.0 (banned).	No
check_sorry(proof_code)	Count sorry placeholders without full verification.	No
lean_machines.list_refinement_chains()	List bundled Event-B refinement chains (Buffer, PushBuffer).	No
lean_machines.to_sva(...)	Translate Lean invariants to SystemVerilog assertions.	No
kairos verify-batch (CLI)	Bulk-verify a directory of .lean files.	No

Free tier never phones home. The only network traffic is when you opt-in to a BYO LLM key. and that traffic goes from your machine directly to your chosen provider, not Athanor.

---

🔒 Paid-tier surface (license required)

Function	What it does
prove(hypothesis, vertical=..., target_file=...)	Tier-1 customer agent entry. NL → IntentV1 → SpecPipeline → Verdict.
session(task_id=...)	Group multiple prove() calls under one task.
fleet.Orchestrator(model=..., worker_models=...)	LLM-backed tier/worker planning across multi-tier specs.
sv.prove, sv.cegar, sv.swarm, sv.invariants	Production RTL verification stack via EBMC.

License gate is fail-closed at every paid callsite: missing license → LicenseScopeError, no silent permissive. Paid customers receive operational deep-dives (orchestrator internals, vertical tactics, runbooks) with their enterprise install tarball.

→ Free vs paid breakdown: docs/sdk-tier-model.md → Threat model: docs/security-model.md → License schema + onboarding: docs/license-schema.md, docs/enterprise-deployment.md

---

CLI

# Preflight (always run first)
python -m kairos doctor               # per-provider green/red + sink resolution

# Free tier
kairos simple-prove "prove c_vector_sharp is positive"
kairos simple-prove --list-patterns
kairos verify-batch ./proofs/

# 🔒 Paid tier (requires license)
kairos prove --nl "..." --vertical ebmc --target-file design.sv
kairos sv-prove --spec design.sv --top-module reno_cca --bound 50

# MCP server for AI agents (Claude Code, Cursor, etc.)
# Exposes lean_solve / lean_race / sv_prove / etc. as MCP tools.
kairos mcp serve

# Audit log inspection (any tier)
kairos audit show --since 7d --denied

→ All subcommands: kairos --help

---

MCP for AI agents

kairos mcp serve is the canonical customer-as-orchestrator entry point: your agent decomposes a hard theorem into sub-lemmas, dispatches each via MCP, composes the closed proofs. kairos provides muscle (drafter race, single-target proof close, axiom audit); your agent provides context (Mathlib knowledge, decomposition strategy).

Add to ~/.claude/.mcp.json:

{
  "mcpServers": {
    "kairos": {
      "command": "kairos",
      "args": ["mcp", "serve"],
      "env": {"ANTHROPIC_API_KEY": "${ANTHROPIC_API_KEY}"}
    }
  }
}

→ Full MCP guide + tool surface + customer-as-orchestrator pattern: docs/customer-onboarding.md#step-5-mcp-server-for-ai-agents

---

Examples

Runnable end-to-end examples live under examples/:

• free-tier-pythia/. simple_prove_template end-to-end with a real Pythia spec.
• sv-multi-bbr3/. 🔒 paid tier, multi-tier RTL verification of BBRv3 starvation properties.
• sv-invariants-telos-reno/. 🔒 paid tier, invariant discovery on a Reno congestion-control RTL.
• sv-hb-graph-two-fifo/. 🔒 paid tier, happens-before graph extraction.

---

Install

pip install athanor-kairos
# or, from source:
pip install git+https://github.com/athanor-ai/athanor-sdk.git@main

You also need lake on PATH for any function that runs Lean verification. Install via elan:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

The paid tier additionally needs ebmc for RTL flows; the docker fallback is auto-used when ebmc is not on PATH.

---

Docs

Topic	Where
Doc index	docs/INDEX.md
Free-tier quickstart	docs/free-tier-quickstart.md
Free vs paid tier model	docs/sdk-tier-model.md
Security model + threat table	docs/security-model.md
License schema	docs/license-schema.md
Enterprise deployment	docs/enterprise-deployment.md
SDK roadmap	docs/sdk-roadmap.md

Internal design docs (post-mortems, decision logs, in-flight design notes) live under docs/internal/. useful for contributors, not required reading for customers.

Paid customers also receive operational deep-dives (orchestrator internals, vertical tactics, runbooks) with their enterprise install tarball. those don't live in this public repo by design.

---

Bundled OSS

kairos vendors three Lean 4 projects (Apache-2.0) so the free tier ships ready to prove. Attribution + upstream pointers in NOTICE.md:

• lean-machines: Event-B refinement framework powering kairos.lean_machines.*.
• lean-machines-examples: Buffer / MQueue / EventB / Algebraic / VDM example specs.
• pythia: tactic library + theorem corpus for probability + statistics, the proof engine behind simple_prove.

---

Pricing + contact

Free tier is free. Paid tier is sales-led. email [e-mail] with your use case. We do not maintain self-serve billing at v1.0.

→ athanor-ai.com