Metadata-Version: 2.4
Name: athanor-sdk
Version: 0.7.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: 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: 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: pytest-cov>=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

# kairos

Formally verified optimization for hardware and software. One command, proven correct.

**Proved equivalent on 3 production RTL blocks with 3-5% area reduction.**

## Quick Start

```bash
pip install athanor-sdk          # imports as: kairos
kairos setup                     # zero-config wizard
kairos optimize block.sv         # your first proved optimization
```

## 4 Verbs: One Command Each

| Command | What it does |
|---------|-------------|
| `kairos explore "8-entry FIFO"` | Generate verified RTL from natural language |
| `kairos optimize block.sv` | Area reduction with formal equivalence proof |
| `kairos verify src/` | 6-layer verification (types, properties, symbolic, drift, specs, mutation) |
| `kairos repair .` | Auto-detect and fix (Python, Lean, Rust, Cedar, merge conflicts) |

## How It Works

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

Every result is formally verified. No optimization ships without proof.
Timing gate rejects optimizations that break timing constraints.

## Hardware Verification (RTL)

```bash
kairos optimize block.sv                    # default: proved equivalent
kairos optimize block.sv --compound 5       # 5 rounds, iterative feedback
kairos optimize block.sv --proposer-backend local  # IP stays on machine
```

## Software Verification (Python / Rust / Lean)

```bash
kairos verify src/                          # 6 layers, all languages
kairos repair .                             # auto-detect and fix
kairos repair file.lean                     # sorry closure (L0-L3 pipeline)
```

## Agent Integration (MCP)

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

Works with Claude Code, Kiro, Cursor, and any MCP-compatible IDE.
6 MCP tools: verify, repair, explore, optimize, help, certify.

## Requirements

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

Optional (for full verification):
- yosys + EBMC (hardware)
- Lean 4 (theorem proving)

Run `kairos doctor` to check your setup.

## Documentation

- [Getting Started](docs/customer/getting-started.md)
- [Enterprise RTL Quickstart](docs/customer/enterprise-rtl-quickstart.md)
- [Security Model](docs/security-model.md)
- [MCP Tool Reference](docs/mcp_tool_reference.md)
- [Architecture](docs/architecture.md)

Built-in: `kairos helper <topic>` for offline docs after install.

## License

Commercial license required for production use. Free evaluation available.
Contact aidan@athanor-ai.com for access.

## Use Cases

**Hardware: reduce FIFO area with formal proof**
```bash
kairos optimize fifo.sv --compound 3
# Result: -5% area, PROVED EQUIVALENT
```

**Hardware: detect clock domain crossing bugs**
```bash
kairos verify --cdc multi_clock_design.sv
# Result: 2 missing synchronizers found, 0 false positives
```

**Software: find null safety violations at scale**
```bash
kairos verify src/
# Result: 6 layers checked, 3 null safety violations, 0 false positives
```

**Software: auto-fix type errors and verify the fix**
```bash
kairos repair src/api.py --fix
# Result: 2 type errors fixed, all fixes verified by re-running tests
```

**Agent integration: verify after every edit**
```json
{"mcpServers": {"kairos": {"command": "kairos", "args": ["mcp", "serve"]}}}
```
Your AI coding agent calls `kairos verify` after every edit. Bugs caught before commit.
