Metadata-Version: 2.4
Name: athanor-sdk
Version: 0.8.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: 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
Description-Content-Type: text/markdown

# kairos

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

**Formally verified equivalence for every optimization. Prove it correct before you ship.**

## Quick Start

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

## Commands

| Command | What it does |
|---------|-------------|
| `kairos spec-gen "8-entry FIFO"` | Natural language to formal SVA specification |
| `kairos arch-explore spec.sv` | Architecture options with tool-backed tradeoffs |
| `kairos optimize block.sv` | Area reduction with formal equivalence proof |
| `kairos optimize --spec spec.sv block.sv` | Multi-step refinement chain with spec |
| `kairos verify src/` | 6-layer verification (types, properties, symbolic, drift, specs, mutation) |
| `kairos repair .` | Auto-detect and fix with severity calibration |
| `kairos sweep rtl_dir/` | Batch optimization across all blocks |

## Full Design Flow

```bash
kairos spec-gen "8-entry FIFO"         # formal SVA specification
kairos arch-explore fifo_spec.sv       # architecture options (tool-backed)
kairos optimize --spec spec.sv fifo.sv # per-block verified optimization
kairos repair src/                     # find remaining bugs
```

Every number from a tool measurement. No LLM estimates as facts.
Area from yosys synthesis, equivalence from EBMC, timing from OpenSTA (when .lib provided).

## 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
kairos optimize block.sv --local-only       # zero network except LLM API
```

## 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.
MCP tools: kairos_verify, kairos_repair, kairos_explore, lean_verify, nki_verify, kairos_formal_explore.

## Requirements

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

Optional (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

- [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.
Visit [athanor-ai.com](https://athanor-ai.com) for access.

## Use Cases

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

**Hardware: detect clock domain crossing bugs**
```bash
kairos verify 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.
