Metadata-Version: 2.4
Name: athanor-sdk
Version: 0.8.11
Summary: Multi-agent verification orchestration -- LLMs propose, formal tools prove, every change is machine-checked
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: beartype>=0.18
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: boto3>=1.26; extra == 'dev'
Requires-Dist: cython>=3.0; extra == 'dev'
Requires-Dist: diff-cover>=8.0; extra == 'dev'
Requires-Dist: hypothesis>=6.0; extra == 'dev'
Requires-Dist: jsonschema>=4.0; extra == 'dev'
Requires-Dist: mcp>=1.0; extra == 'dev'
Requires-Dist: pytest-cov>=4.0; extra == 'dev'
Requires-Dist: pytest-xdist>=3.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
Provides-Extra: types
Requires-Dist: mypy>=1.0; extra == 'types'
Provides-Extra: verify
Requires-Dist: crosshair-tool>=0.0.60; extra == 'verify'
Description-Content-Type: text/markdown

# kairos

**Multi-agent verification orchestration for hardware and software.**

LLMs can propose RTL optimizations, but they cannot prove those optimizations are correct. A single model call that claims "area reduced by 12%" has no way to guarantee functional equivalence with the original design. Kairos closes that gap: it orchestrates specialized agents (proposer, reviewer, counterexample analyst) through formal verification tools (EBMC, yosys, Lean) in a closed loop where every proposed change is machine-checked before acceptance.

`kairos optimize block.sv` runs a multi-agent loop: the proposer generates candidates, EBMC k-induction proves functional equivalence, yosys measures the real area delta, and the reviewer challenges the result. What ships is not what the LLM said works -- it is what the formal tools proved correct.

Kairos is a CLI and MCP server. Connect it to Claude Code, Kiro, or Cursor, and your agent gets 40+ verification tools that return machine-checked results, not LLM opinions.

### Why agents need guardrails

Every agent in the kairos loop has a different role and a different incentive. The proposer optimizes, the reviewer challenges, the counterexample analyst actively tries to break the proposal. Only changes that survive all three reach formal verification. And formal verification is not simulation or testing -- it is mathematical proof over all possible inputs.

The guardrail stack:
- **Pre-verification gates** reject bad proposals before they reach formal tools: structural gate (cell count must decrease), toggle power gate (no >20% power regression)
- **Bounded model checking** (EBMC) proves properties hold for all states up to depth k
- **Equivalence checking** (yosys) proves the optimized netlist matches the original
- **Counterexample generation** refutes invalid proposals with concrete failing traces
- **Trust boundary** separates LLM-touching code from certificate generation (AST-lint enforced)
- **Block memory** tracks refuted approaches so agents cannot re-propose known failures
- **Certificate chain** with sha256 provenance from source through proof to output

### Focus areas

| Domain | Verification engine | What kairos checks |
|--------|--------------------|--------------------|
| **General software** | mypy, hypothesis, CrossHair, mutmut | Types, properties, symbolic contracts, mutation testing |
| **Chip design (RTL)** | EBMC, yosys | Equivalence, safety properties, area/power optimization |
| **Accelerator kernels** | NKI runtime, Lean 4 | Custom kernel correctness, formal proof gate |
| **Networking protocols** | EBMC, z3 | Congestion control properties (BBR, CUBIC, Reno convergence) |
| **Theorem proving** | Lean 4 | Proof verification, sorry closure, axiom auditing |
| **Authorization policy** | Cedar | permit/forbid policy correctness |

Kairos is built by kairos. We use our own verification and anti-hallucination tools to develop, test, and ship kairos itself. Every bug found by `kairos repair --review` on our own codebase makes the tool stronger.

## Quick start

### pip install

```bash
pip install athanor-sdk          # imports as: kairos
pip install athanor-sdk[types]   # adds mypy for Python type checking
kairos setup                     # zero-config wizard
kairos doctor                    # verify your environment

# Verify any codebase
kairos verify block.sv           # chip design (RTL)
kairos verify kernel.py          # accelerator kernel
kairos verify src/               # Python (types + properties + mutation)
kairos repair --review .         # find bugs across the whole project
```

### Docker (includes all verification engines)

```bash
# Authenticate with GitHub Container Registry (one-time setup)
echo $GITHUB_TOKEN | docker login ghcr.io -u USERNAME --password-stdin

docker pull ghcr.io/athanor-ai/kairos:latest
docker run --rm -v $PWD:/work ghcr.io/athanor-ai/kairos:latest verify /work/block.sv
docker run --rm -v $PWD:/work ghcr.io/athanor-ai/kairos:latest verify /work/train.py
docker run --rm -e ANTHROPIC_API_KEY -v $PWD:/work ghcr.io/athanor-ai/kairos:latest optimize /work/block.sv
```

The Docker image includes yosys, EBMC, verilator, and all other engines. No additional installs needed. `GITHUB_TOKEN` needs `read:packages` scope (create at github.com/settings/tokens).

## Commands

### design -- create RTL from natural language

```bash
kairos design "8-entry FIFO with sync reset"     # spec + architecture + RTL
kairos design --spec fifo_spec.sv                 # skip spec-gen, start from SVA
kairos design "pipelined ALU" --output ./alu/     # custom output directory
```

### optimize -- area/power reduction with formal proof

```bash
kairos optimize block.sv                          # propose + verify + measure
kairos optimize block.sv --estimate-only          # preview strategies + cost, no LLM
kairos optimize block.sv --compound 5             # 5 iterative rounds
kairos optimize block.sv --liberty cells.lib      # technology-mapped cell counts
kairos optimize block.sv --local-only             # zero network except LLM API
kairos optimize kernel.py                         # auto-detects NKI kernels
```

### verify -- auto-detect domain, multi-layer checking

```bash
kairos verify block.sv                            # RTL: yosys + EBMC bounded model check
kairos verify src/                                # directory: walks all files
kairos verify my_cca.py                           # Python CCA: telos + types + mutation (auto-detected)
kairos verify proof.lean                          # Lean: lake build + sorry check
```

Auto-detects the verification domain from file content, not just
extension. A Python file with networking patterns (cwnd, ssthresh,
pacing_rate) gets telos protocol verification THEN Python type
checking and mutation testing -- stacked, not either/or.

### repair -- find + fix + verify

```bash
kairos repair block.sv                            # detect issues, propose fixes, verify
kairos repair --review block.sv                   # diagnose only, no changes
kairos repair --focus security src/               # focus on security findings
```

### explore -- fork and compare design variants

```bash
kairos explore block.sv                           # architecture exploration
kairos explore block.sv --fork area timing power  # parallel variant comparison
```

### doctor -- environment health check

```bash
kairos doctor                                     # check deps, license, engines, models
kairos doctor --json                              # machine-readable output
```

### support-bundle -- collect diagnostics for debugging

```bash
kairos support-bundle                             # human-readable diagnostic info
kairos support-bundle --json                      # machine-readable for support tickets
```

### quickstart -- zero to first verify

```bash
kairos quickstart                                 # detect env, install deps, run first verify
```

### watch -- continuous verification

```bash
kairos watch .                                    # re-verify on file change
kairos watch src/ --interval 30                   # custom scan interval
```

### setup -- first-run configuration

```bash
kairos setup                                      # interactive wizard
kairos setup --user-install                       # install EBMC to ~/.local/bin (no sudo)
kairos setup --check                              # validate current config
```

## How it works

1. **Propose**: LLM generates optimization candidates (local or cloud)
2. **Verify**: EBMC k-induction proves functional equivalence
3. **Measure**: yosys synthesis confirms real area reduction
4. **Report**: honest verdict with claim verification

Every measurement from a tool, not an LLM estimate. Area from yosys
synthesis, equivalence from EBMC, timing from OpenSTA (when .lib provided).

## Configuration (kairos.yaml)

Drop a `kairos.yaml` in your project root:

```yaml
model: claude-sonnet-4-6

methodology:
  verification:
    require_equivalence_proof: true
    minimum_bound_k: 10
  certificate:
    require_all_properties_proved: true

agents:
  reviewer:
    enabled: true
    severity_threshold: medium
```

Precedence: CLI flags > kairos.yaml > environment variables > defaults.

## Agent integration (MCP)

```json
{
  "mcpServers": {
    "kairos": {
      "command": "kairos",
      "args": ["mcp", "serve"]
    }
  }
}
```

Works with Claude Code, Kiro, Cursor, and any MCP-compatible IDE.
41 tools available including kairos_optimize, kairos_verify,
kairos_repair, kairos_explore, and kairos_doctor.

## Local-only mode

```bash
kairos optimize block.sv --local-only
kairos optimize block.sv --proposer-backend local  # RTL never leaves machine
```

No trace upload, no telemetry. Only the LLM API call leaves your machine.
Use `--proposer-backend local` with ollama/vLLM for full air-gapped operation.

## Requirements

- Python 3.10+
- `kairos setup` installs everything else

Optional extras:
- `pip install athanor-sdk[types]`: mypy for Python type checking layer
- `pip install athanor-sdk[verify]`: CrossHair for symbolic contract checking
- `pip install athanor-sdk[mcp]`: MCP server for IDE integration

Optional engines (for full verification):
- yosys + EBMC (hardware equivalence)
- Lean 4 (theorem proving)
- OpenSTA (timing analysis, requires Liberty .lib)

Run `kairos doctor` to check your setup.

## Documentation

In Docker: see `/opt/kairos-docs/` for bundled guides.

- Getting Started (`getting-started.md`)
- Installation Guide (`installation.md`)
- Enterprise RTL Quickstart (`enterprise-rtl-quickstart.md`)

## License

Commercial license required for production use. Free evaluation available.
Visit [athanor-ai.com](https://athanor-ai.com) for access.
