athanor-sdk 0.7.5

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

kairos

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

21+ blocks optimized with formally verified equivalence, up to 76% area reduction.

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

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: -5% area, 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.