athanor-sdk 0.8.1

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

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

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

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)

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)

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. 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
• 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. Visit athanor-ai.com for access.

Use Cases

Hardware: reduce FIFO area with formal proof

kairos optimize fifo.sv --compound 3
# Result: area reduced, PROVED EQUIVALENT

Hardware: detect clock domain crossing bugs

kairos verify 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.