athanor-sdk 0.7.0

Formal verification as agentic training signal — CLI + self-hosted runner

kairos

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

PROVED EQUIVALENT on production Annapurna RTL:

• AP_ALU_US: 13,252 → 12,728 cells (-3.95%)
• AP_REG_FIFO_US: 151/151 cells verified
• AP_REG_FIFO_REPL: 695 → 659 cells (-5.18%)

Quick Start

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)

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)

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)

{
  "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
• Enterprise RTL Quickstart
• Security Model
• MCP Tool Reference
• Architecture

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

License

Commercial license required for production use. Free evaluation available. Contact [e-mail] for access.

Use Cases

Hardware: reduce FIFO area with formal proof

kairos optimize fifo.sv --compound 3
# Result: -5.18% area (695 -> 659 cells), PROVED EQUIVALENT

Hardware: detect clock domain crossing bugs

kairos verify --cdc multi_clock_design.sv
# Result: 2 missing synchronizers found, 0 false positives

Software: find null safety violations at scale

kairos verify src/
# Result: 6 layers checked, 3 null safety violations, 0 false positives

Software: auto-fix type errors and verify the fix

kairos repair src/api.py --fix
# Result: 2 type errors fixed, all fixes verified by re-running tests

Agent integration: verify after every edit

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

Your AI coding agent calls kairos verify after every edit. Bugs caught before commit.