Metadata-Version: 2.4
Name: athanor-sdk
Version: 0.6.1
Summary: Formal verification as agentic training signal — CLI + self-hosted runner
Project-URL: Homepage, https://athanor-ai.com
Project-URL: Repository, https://github.com/athanor-ai/athanor-kairos
Author: Athanor AI
License-Expression: LicenseRef-Proprietary
License-File: LICENSE
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Requires-Python: >=3.9
Requires-Dist: cryptography>=41.0
Requires-Dist: litellm>=1.50.0
Requires-Dist: pydantic>=2.0
Requires-Dist: pyyaml>=6.0
Requires-Dist: tomli>=2.0; python_version < '3.11'
Provides-Extra: cedar
Provides-Extra: dev
Requires-Dist: cython>=3.0; extra == 'dev'
Requires-Dist: hypothesis>=6.0; extra == 'dev'
Requires-Dist: jsonschema>=4.0; extra == 'dev'
Requires-Dist: pytest>=7.0; extra == 'dev'
Requires-Dist: ruff>=0.5; extra == 'dev'
Requires-Dist: setuptools>=60; extra == 'dev'
Requires-Dist: tomli>=2.0; (python_version < '3.11') and extra == 'dev'
Provides-Extra: mcp
Requires-Dist: mcp>=1.0; extra == 'mcp'
Provides-Extra: multi-model
Provides-Extra: telos
Description-Content-Type: text/markdown

<p align="center">
  <img src="logo.svg" width="64" height="64" alt="Athanor">
</p>

<h1 align="center">kairos</h1>

<p align="center"><sub>The SDK from <a href="https://athanor-ai.com">Athanor AI</a>. Distributed as <code>athanor-sdk</code> on PyPI; imports as <code>kairos</code>.</sub></p>

<p align="center">
  <strong>Prove properties of your code in plain English.</strong><br>
  Free tier: zero phone-home, no license required, Lean stays hidden.<br>
  Paid tier: full RTL verification stack + LLM-orchestrated multi-tier reasoning.<br><br>
  <a href="https://athanor-ai.com">athanor-ai.com</a>
</p>

---

## Free tier in 30 seconds

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

```python
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](docs/byo-model.md). The SDK supports **any model**: Anthropic (Direct / Azure / Bedrock), OpenAI, Gemini, Together, Fireworks, Ollama, vLLM, or any OpenAI-compatible endpoint. Pass the model string; kairos routes it. The SDK never sees the key, calls go directly customer to provider.

AWS customers: run `kairos init aws` for the 5-prompt onboarding wizard that chains Bedrock-key + S3 trace storage + Postgres run-history setup into one flow. Or set each piece individually: `kairos config set bedrock-key <key>` / `kairos config s3 <bucket>` / `kairos config db <conn>`. All stored at `~/.athanor/config.json` (chmod 600). See [docs/byo-model.md](docs/byo-model.md) for the full resolution order.

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

```bash
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`](docs/free-tier-quickstart.md)
→ **Doc map:** [`docs/INDEX.md`](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`](docs/sdk-tier-model.md)
→ **Threat model:** [`docs/security-model.md`](docs/security-model.md)
→ **License schema + onboarding:** [`docs/license-schema.md`](docs/license-schema.md), [`docs/enterprise-deployment.md`](docs/enterprise-deployment.md)

---

## CLI

```bash
# 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`:

```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`](docs/customer-onboarding.md#step-5-mcp-server-for-ai-agents-claude-code-cursor-etc)

---

## Examples

Runnable end-to-end examples live under [`examples/`](examples/):

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

---

## Install

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

You also need `lake` on `PATH` for any function that runs Lean verification. Install via [elan](https://leanprover-community.github.io/get_started.html):

```bash
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`](docs/INDEX.md) |
| Free-tier quickstart | [`docs/free-tier-quickstart.md`](docs/free-tier-quickstart.md) |
| Free vs paid tier model | [`docs/sdk-tier-model.md`](docs/sdk-tier-model.md) |
| Security model + threat table | [`docs/security-model.md`](docs/security-model.md) |
| License schema | [`docs/license-schema.md`](docs/license-schema.md) |
| Enterprise deployment | [`docs/enterprise-deployment.md`](docs/enterprise-deployment.md) |
| SDK roadmap | [`docs/sdk-roadmap.md`](docs/sdk-roadmap.md) |

Internal design docs (post-mortems, decision logs, in-flight design notes) live under [`docs/internal/`](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`](NOTICE.md):

- [`lean-machines`](https://github.com/lean-machines-central/lean-machines): Event-B refinement framework powering `kairos.lean_machines.*`.
- [`lean-machines-examples`](https://github.com/lean-machines-central/lean-machines-examples): Buffer / MQueue / EventB / Algebraic / VDM example specs.
- [`pythia`](https://github.com/athanor-ai/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. Contact your Athanor team with your use case. We do not maintain self-serve billing at v1.0.

→ [athanor-ai.com](https://athanor-ai.com)
