Metadata-Version: 2.4
Name: athanor-sdk
Version: 0.8.18
Summary: CLI for customer-controlled RTL optimization, verification reports, and reproducible run artifacts
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 :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Requires-Python: >=3.12
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'
Requires-Dist: hypothesis>=6.0; extra == 'verify'
Requires-Dist: mutmut>=3.0; 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 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, formal engines prove functional equivalence, synthesis tools measure 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 with optional MCP server integration. Connect it to
Claude Code, Kiro, or Cursor with `athanor-sdk[mcp]`, and your agent
gets verification tools that return machine-checked results, not LLM
opinions.

Every accepted change is machine-checked. No change ships without formal proof.

## Quick start

### pip install

```bash
pip install athanor-sdk                 # imports as: kairos
pip install 'athanor-sdk[types,verify]' # full Python verification deps

# If 'kairos' is not found after install, add ~/.local/bin to PATH:
# export PATH="$HOME/.local/bin:$PATH"

kairos setup                     # zero-config wizard
kairos doctor                    # verify your environment

# Verify any codebase (no LLM required)
kairos verify block.sv           # chip design (RTL)
kairos verify kernel.py          # accelerator kernel
kairos verify src/               # Python layers backed by installed extras

# Find + fix bugs (requires LLM API key)
kairos repair --review .         # diagnose issues across the project
```

Base `pip install athanor-sdk` gives the CLI, core libraries, and health
checks. Full Python verification needs `athanor-sdk[types,verify]`; MCP
IDE integration needs `athanor-sdk[mcp]`. RTL verification also needs backend engines, which are included in the Docker image.

### Docker (includes all verification engines)

```bash
# Docker image provided during enterprise onboarding
docker run --rm -v $PWD:/work kairos:latest verify /work/block.sv
docker run --rm -v $PWD:/work kairos:latest optimize /work/block.sv
```

The Docker image includes all verification backends. No additional installs needed. Image access is provided during enterprise onboarding.

## Commands

### optimize -- area reduction with formal equivalence proof (requires LLM)

```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             # no trace upload; LLM still needs network
kairos optimize kernel.py                         # auto-detects NKI kernels (AWS Neuron NKI dispatch supported)
```

### verify -- per-property PROVED / REFUTED / INCONCLUSIVE (no LLM required)

```bash
kairos verify block.sv                            # RTL: formal bounded model check + k-induction
kairos verify src/                                # directory: walks all files
kairos verify my_cca.py                           # Python CCA: telos + installed Python layers
kairos verify contract.txt                        # proof contract: build + consistency check
```

Reports per-property verdicts (bounded model checking and
k-induction). Theorem provers are used as triage hints, not certifiers. Never
demotes an inconclusive to a pass. Auto-detects the verification
domain from file content, not just extension.

### repair -- find + fix + verify (requires LLM)

```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
```

### doctor -- environment health check

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

### quickstart -- zero to first verify

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

### setup -- first-run configuration

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

### mcp -- IDE agent integration

```bash
kairos mcp serve                                  # start the MCP server for supported IDE agents
```

## Example Designs

These examples live in the source repository, not in the minimal PyPI
wheel. Run them from a repo checkout, or use the Docker image with a
mounted checkout:

```bash
git clone https://github.com/athanor-ai/athanor-kairos.git
cd athanor-kairos

# Combinational (optimize works well)
kairos optimize examples/synthetic/hamming_encoder.sv    # -28.57% area reduction
kairos optimize examples/synthetic/alu_onehot.sv         # -10.83% area reduction

# Sequential networking
kairos optimize examples/sv-networking-reno/reno_sender.sv  # -54.24% area reduction

# Verification canaries (known-bad, should REFUTE)
kairos verify examples/golden/alu_wrong_op.sv            # wrong ALU operation → REFUTED
kairos verify examples/golden/fifo_off_by_one.sv         # FIFO pointer bug → REFUTED
kairos verify examples/golden/counter_no_reset.sv        # missing reset → REFUTED
```

More designs in `examples/benchmarks/rtllm/` (multiplier, divider, FSM, signal processing).
See `examples/golden/README.md` for the full canary matrix with honest measured verdicts.

## How it works

1. **Propose**: LLM generates optimization candidates (local or cloud)
2. **Verify**: formal engines report per-property PROVED / REFUTED / INCONCLUSIVE
3. **Measure**: synthesis tools measure the actual area delta. Pass `--liberty cells.lib` for technology-mapped counts
4. **Accept or reject**: only accepted when formal equivalence is proved AND a measured cell reduction is achieved. Fails closed on unmeasured cells, undischarged assumptions, and incomplete proofs

Every measurement comes from a tool, not an LLM estimate. Every certificate records its measurement conditions so results are reproducible.

## 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]`: Hypothesis, CrossHair, and mutmut for Python property/symbolic/mutation layers
- `pip install athanor-sdk[mcp]`: MCP server for IDE integration

Run `kairos doctor` to check your setup. All required backends are included in the Docker image.

## 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.
