CLI and script integration for verification of hardware and software.
Kairos helps hardware teams verify RTL, evaluate optimization candidates, and inspect repair proposals with formal evidence instead of simulation-only claims. Customer deployments are provisioned by Athanor with a licensed image or private package, customer-specific credentials, and an onboarding runbook for the customer's environment.
There is no current public PyPI install path for Kairos. Public pages should not be read as an open-source SDK release.
Your Athanor contact provides the image or package identifier, registry access, and license material for your evaluation. Use those provisioned values rather than installing an unmaintained public package.
# Values are supplied during enterprise onboarding $ <registry-login-command-from-onboarding> $ docker run --rm -v "$PWD":/work <customer-kairos-image> doctor
kairos doctor should be the first customer run: it confirms the license, toolchain, model routing, and environment assumptions before a verification or optimization result is trusted.
After onboarding, mount the design directory into the provisioned Kairos image and run the same CLI commands against your RTL.
# Verify an RTL design $ docker run --rm -v "$PWD":/work <customer-kairos-image> verify /work/block.sv # Inspect environment and license state $ docker run --rm -v "$PWD":/work <customer-kairos-image> doctor # Evaluate optimization candidates when model access is configured $ docker run --rm -v "$PWD":/work <customer-kairos-image> optimize /work/block.sv
Verification output reports the result, the evidence scope, and next actions. Optimization claims are tied to replayable proof and measurement receipts for the exact candidate and toolchain.
All examples here use public open-source RISC-V designs and published artifact packages. Anyone can inspect and re-verify the receipts below: no license or account required.
# Anyone can inspect the public Ibex receipts without a Kairos license $ git clone https://github.com/athanor-ai/ibex-athanor.git $ cd ibex-athanor $ python3 athanor/verify_public_receipts.py
| Promoted win | Ibex ibex_fetch_fifo is an accepted module-local public row. The packet reports lower cell counts under the recorded flows, flat activity, bounded sequential checks, temporal induction, an independent SBY/ABC PDR leg, and a bad-mutant non-vacuity bite. It is not a whole-core ibex_top claim. |
| Published refusal | OpenC910 ct_fifo is a proof-evidence packet, not a promoted optimization win. Its proof artifacts, SHA-bound files, pinned logs, and biting mutants are public, and its own metric screen refuses promotion because timing regresses. The raw exact-output induction did not close; the positive proof authority is the relation miter. The packet says to treat it as a replayable proof artifact plus a metric hard negative. |
| Scoped subsystem evidence | OpenC910 ct_pmp_top lifts the scoped ct_pmp_acc NAPOT-mask candidate through a subsystem-top packet. Packet-replay evidence, reproduced byte-exact by a non-author, includes a closed same-state proof with a proof-mutant rejection. The packet's own status block states the current product classifies it as a gap: the PPA, timing, simulation, and toggle legs are unavailable, and the metric negative control does not discriminate. It is not a whole-C910, ISA, privilege-model, signoff-timing, workload-power, or Lean theorem claim. |
| What holds | The exact property or relation that the packet establishes, including whether it is bounded or unbounded. |
| What was assumed | The reset, reachability, or relation assumptions behind the proof. The Ibex FIFO packet derives occupancy from reset and reachability instead of supplying it externally. |
| What is not covered | Scope limits travel with the result. Module-local evidence is not a whole-core, ISA, signoff, or customer-design claim. |
| How to check it | Run the public receipt verifier or inspect the linked SHA-bound logs and negative controls. |
Every published packet carries a machine-readable receipt beside its pinned logs. The fields below are the load-bearing ones, shown with their real values from the OpenC910 ct_fifo packet; every packet follows the same shape.
status |
The claim class in one string. For ct_fifo: module_local_visible_output_equivalence_packet. The status names the boundary of the claim, not a marketing word. |
customer_ready |
A boolean the packet declares about itself. ct_fifo ships customer_ready: false even though its proof legs close, because its own metric screen refused promotion. A receipt that can say no about itself is the point. |
known_boundaries |
The scope limits, in the packet, as data. For ct_fifo the first entry records that the exact gold/gate visible-output proof is bounded to seq12 in the exact miter, and that the closed unbounded proof runs over state-exposed copies. Limits travel with the result they bound. |
artifact_hashes + SHA256SUMS |
Every file the receipt cites is hash-pinned. Change a byte in a log or a netlist and the packet no longer verifies. This is what the public verifier checks. |
proof_receipts / area_receipts |
Pointers from each claim to the exact pinned log that backs it, so a number is never further than one hop from the tool output that produced it. |
toolchain |
The pinned suite the packet was measured with, so a replay uses the toolchain that produced the numbers rather than whatever is installed. |
These lines are quoted byte-for-byte from the pinned logs in the public packets. Each carries its scope; none of them is a whole-core, ISA, or signoff claim.
# Bounded equivalence, Ibex fetch FIFO packet: bounded_k16 / _k20 / _k30 logs.
# A bounded pass establishes finite-depth coverage to the stated depth, nothing deeper.
SAT proof finished - no model found: SUCCESS!
# Unbounded leg, OpenC910 ct_fifo relation miter (state-exposed copies, seq8):
# temporal induction closes the proof for every reachable state, under the
# packet's stated relation assumptions.
Induction step proven: SUCCESS!
# Non-vacuity controls, OpenC910 ct_fifo packet: the deliberately broken mutant MUST fail.
# A red here is the desired result; it proves the proof can detect a real bug.
SAT proof finished - model found: FAIL!
SAT temporal induction proof finished - model found for base case: FAIL!
A green proof line only counts alongside its failing mutant: the pair shows the instrument both proves the real design and rejects a broken one. The Ibex FIFO packet adds an independent SBY/ABC PDR leg on top of these, and the ct_fifo packet publishes its raw exact-output induction as a non-closure boundary rather than hiding it. What a packet cannot prove, it says.
Live Kairos command transcripts are intentionally not shown here until the shipped image reports success only with an explicit bound and non-vacuity signal. Until then, the packet verifier and replay scripts are their own stdlib tooling and do not invoke Kairos; product-driven replay ships later as a Kairos command.
The customer-visible CLI is grouped by workflow below. Commands that make proof or optimization claims either emit a scoped verdict directly or point to a replayable package that carries its own evidence boundary.
kairos quickstart |
Runs the first-time onboarding flow: detects the local environment, checks engines and configuration, runs doctor, then verifies a bundled RTL sample. Use it on a fresh provisioned image before running customer RTL. |
kairos setup |
Configures Kairos for the current seat. Use --check to validate without changing configuration, or --user-install when engines should be placed under ~/.local/bin. |
kairos doctor |
Checks license, model routing, local proof/EDA tools, package installation, telemetry routing, and update status. Use --verification-only for local proof readiness, --deep for smoke tests, --strict to fail on skipped checks, and --json for automation. |
kairos eval-license |
Writes an evaluation-license payload for trial setup. Production customer trials are signed by Athanor; after receiving license material, run kairos doctor to verify the active license path. |
kairos verify |
Verifies an RTL design, formal proof source, certificate bundle, or design-closure directory. Common inputs are block.sv, --deps, -I, -D, --spec, --discover, and --run-replay. Text output reports the scoped verdict and next action; --json emits the same verdict envelope for scripts. |
kairos verify-change |
Adjudicates an optimization receipt package or a gold/candidate RTL pair. Use --out to write a replayable receipt package, --run-local-tools to collect proof and PPA legs, --negative-control to prove the gate can fail, and --run-replay before relying on the package. Output names the claim class, product disposition, missing evidence, and next action. |
kairos optimize |
Proposes and checks RTL optimization candidates. Inputs include RTL, --deps, include directories, defines, parameters, model/backend selection, objective, spend budget, compound rounds, and optional Liberty files. --plan-only and --estimate-only do not execute the campaign; --out writes a durable run directory; --verify-change-out runs the handoff into a receipt package. |
kairos certify-customer |
Checks a <block>_kairos_cert.tar.gz package emitted by kairos optimize. The report covers artifact integrity, customer-safety surface, proof-shape ingest, claim taxonomy, and whether the package is customer-promotable. Add --json for a machine-readable report. |
kairos repair |
Diagnoses and repairs RTL or repository issues, with --review for diagnose-only, --fix for applying repairs, --dry-run for patch previews, --batch for directory work, and --json for structured findings. |
kairos benchmarks list |
Lists the shipped open-source silicon benchmark catalog with case id, design, command, source repository, license, expected statuses, claim boundary, and docs pointer. Use --json when selecting cases from automation. |
kairos benchmarks show <case> |
Prints one benchmark case and the exact copy-pasteable Kairos command with bundled fixture paths and dependencies resolved. This is the preferred path for reproducing catalog rows without hand-transcribing flags. |
kairos mcp serve |
Starts the stdio MCP server for Claude Code, Cursor, Cline, OpenHands, and supported IDE agents. Base SDK tools are available to every installation; licensed customers see the paid Kairos tools for their seat. |
kairos mcp install |
Auto-detects a supported IDE and installs Kairos as an MCP server. Use --target to force claude-code, cursor, vscode, or desktop. |
Integrate kairos into scripts via the CLI.
import subprocess, json # Verify an RTL design result = subprocess.run( ["kairos", "verify", "arbiter.sv", "--json"], capture_output=True, text=True, ) verdict = json.loads(result.stdout) # Inspect results print(verdict["status"]) # scoped result status print(verdict["detail"]) # per-property breakdown
$ kairos mcp serve
Works with Claude Code, Kiro, Cursor, and any MCP-compatible IDE. Verification tools return machine-checked results directly in your editor.
# Docker image and registry access are provided during enterprise onboarding $ <registry-login-command-from-onboarding> $ docker run --rm -v "$PWD":/work <customer-kairos-image> verify /work/block.sv
The licensed image includes the RTL verification toolchain for the provisioned customer workflow. Image access, license handling, and deployment controls are documented during onboarding.