proving or disproving computational claims, end to end.
AI now writes faster than anyone can review. Athanor builds the infrastructure that decides whether it is right. Our first system is Kairos.
state the property.
A claim is anything you want to be true about a program, a circuit, or a protocol. It might express equivalence, safety, or a bound. State it once and state it precisely. Malformed specs are refused at the door.
the model proposes.
the math decides.
AI drafts the candidate, proof, or optimization. Kairos orchestrates bounded checks, temporal induction, and Lean 4 obligations until the claim closes. The model is never the authority; the checker is.
proved, refuted, or inconclusive. never promoted.
A replayable proof term or a concrete counterexample, stamped with the tool versions and conditions that produced it. When a proof doesn't close, it says so.
optimize, then prove it again.
Optimization runs the same loop. Each candidate must be proved equivalent and measured by synthesis tools. If either check fails, its own receipt refuses it.
we build kairos.
A verification engine for hardware and software. Accepted results carry a machine-checked proof, a real measurement, and the conditions needed to reproduce both. Every packet also states what it cannot prove.
what happens when the proof
is the ground truth.
Congestion Control: A Machine-Checked Refutation of BBRv3 Starvation
Five independent verifiers close the same closed-form bound on starvation-onset time. Every verdict is reproducible with one command.
fix_arb_lock: end-to-end solve walkthrough
Seven assertions discharged in 0.278 s; the Lean layer catches what bounded model-checking could not.
Does a formal-verification layer improve kernel quality?
Kernels that pass every seeded test still fail the universal correctness theorem.
Formal verification of dopamine reward prediction
Formal invariants disambiguate causal credit from correlation.
claims in. certificates out.
Kairos proves or refutes computational claims across hardware and software. Each verdict comes with the artifact that justifies it: a replayable proof or a concrete counterexample.
three verdicts.
three artifacts.
Every verdict ships with the thing that justifies it. Nothing between the model and the certificate is trusted on the model's word.
A replayable proof
An equivalence proof, an induction certificate, or a Lean 4 proof term. The kernel checks it, you can rerun it, and the receipt pins the toolchain that produced it.
A concrete counterexample
The exact input sequence, policy request, or state that breaks the claim. A refutation is a first-class result. It is the bug you would otherwise ship.
An honest boundary
Bounded coverage to a stated depth, a leg that did not close, or a metric screen that refused. The packet keeps those limits visible.
what a packet cannot prove, it says.
Verdicts are never promoted. Inconclusive stays inconclusive; published refusals show exactly where proofs don't close.
Output preserves evidence scope, limitations, and next actions. Inconclusive or unsupported results stay visible.
Statistical testing is never labeled as formal proof. Certificate labels disclose the verification method.
Every certificate records the tool versions, synthesis recipe, and other measurement conditions needed for reproduction.
Accepted optimizations require formal equivalence proof and measured area reduction. No exceptions.
open silicon,
public receipts.
The examples use public RISC-V designs and published artifact packages. Anyone can inspect and re-verify the receipts without a license or account.
| packet | status | what it establishes |
|---|---|---|
ibex_fetch_fifo | promoted | Module-local accepted row: lower cell counts under recorded flows, bounded sequential checks, temporal induction, an independent SBY/ABC PDR leg, bad-mutant non-vacuity bite. Not a whole-core claim. |
ct_fifo | refused | Proof-evidence packet whose own metric screen refuses promotion because timing regresses. It ships customer_ready: false even though its proof legs close. |
ct_pmp_top | gap | Closed same-state proof with proof-mutant rejection, reproduced byte-exact by a non-author. PPA, timing, and toggle legs unavailable. |
provisioned,
not pip-installed.
Kairos is licensed per customer environment. Evaluation access is issued during onboarding.
Share deployment details
Tell your Athanor contact about your environment. Evaluation access is issued during onboarding.
Receive a licensed image
A private image or package, credentials, and a runbook provisioned for your environment. No public install path.
Run kairos doctor
Confirms license, toolchain, model routing, and environment assumptions before any result is trusted.
--local-only for air-gapped operation; customer designs are never used for training. Security & data handling →the theorem-proving foundation kairos builds on.
An open-source Lean 4 tactic library: automated proof strategies, sorry closure, axiom auditing, and proof obligation tracking. Use it standalone or as part of the Kairos pipeline.
-- a real theorem from Pythia's engineering library import Pythia.Engineering.PowerDissipation open Pythia.Engineering example (I R : ℝ) (hR : 0 ≤ R) : 0 ≤ powerDissipation I R := by pythia #print axioms Pythia.Engineering.power_dissipation_nonneg [propext, Classical.choice, Quot.sound]
Tactic library
Automated proof strategies for Lean 4 including omega, bv_decide, simp chains, and custom domain-specific tactics.
Proof verification
Sorry closure, axiom auditing, and proof obligation tracking. Every proof is machine-checked by the Lean kernel.
Open source
Apache-2.0 licensed. Use it standalone or as part of the Kairos verification pipeline. Contributions welcome.
Verified against the Pythia repository's pinned Lean toolchain.
Athanor writing and technical reports
hardware verification
3 reportsEnd-to-end solve of a bus-arbiter liveness task
One task, followed from spec intake to shipped bundle. Three malformed specs are refused at the door without invoking a generation model; EBMC discharges the seven SystemVerilog assertions in 0.278 s; the Lean layer catches a misstated fairness theorem that bounded model-checking could not catch.
26-task RTL correctness benchmark
26 SystemVerilog and NuSMV repair tasks scored by EBMC, with Lean 4 theorem obligations on the five tasks that require universally-quantified correctness. Model-checked properties either prove or they don't.
Universally-quantified correctness for AI-generated NKI kernels
AI-generated accelerator kernels pass seeded property tests and still produce silently wrong output on nearby input shapes. A universally-quantified correctness theorem rejects kernels that cannot discharge it.
software systems
4 reportsThree Cedar tasks where correctness beats testing
Authorization policies that pass unit tests still admit privilege-escalation paths. An adversarial policy audit, a photo-sharing policy debug, and a Lean 4 proof of Cedar schema validation soundness.
Machine-checked refutation of BBRv3 starvation
Five independent verifiers close the same closed-form bound on starvation-onset time. Every verdict is reproducible with one command.
Where consensus implementations drift from their specifications
Raft, Paxos, PBFT, and 2PC implementations are checked against safety, liveness, and crash-recovery obligations after realistic protocol drift is introduced.
What breaks when models port C to Rust
Twenty-eight sparse linear algebra and vector-math tasks test bit-exact correctness, performance parity, and ownership-safe translation.
life sciences
1 reportFormal verification of dopamine reward prediction
Multi-agent credit assignment verified against formal reward-prediction invariants. Demonstrates how formal methods disambiguate causal credit from correlation in neural reward pathways.
kairos documentation.
CLI and script integration for verification of hardware and software.
01overview
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.
02access
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> doctorkairos 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.
03quick start
After onboarding, mount the design directory into the provisioned 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 # 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.
04open-source silicon demonstrations
All examples use public open-source RISC-V designs and published artifact packages. Anyone can inspect and re-verify the receipts without a license or account.
$ git clone https://github.com/athanor-ai/ibex-athanor.git $ cd ibex-athanor $ python3 athanor/verify_public_receipts.py
| packet | status | what it establishes |
|---|---|---|
ibex_fetch_fifo | promoted | Module-local accepted row: lower cell counts under recorded flows, bounded sequential checks, temporal induction, an independent SBY/ABC PDR leg, bad-mutant non-vacuity bite. Not a whole-core ibex_top claim. |
ct_fifo | refused | Proof-evidence packet; its own metric screen refuses promotion because timing regresses. Positive proof authority is the relation miter; raw exact-output induction did not close. |
ct_pmp_top | gap | Closed same-state proof with proof-mutant rejection, reproduced byte-exact by a non-author. PPA, timing, simulation and toggle legs unavailable. |
how to read a receipt
| what holds | The exact property or relation 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. |
inside a receipt
Every published packet carries a machine-readable receipt beside its pinned logs. The load-bearing fields, with their real values from the OpenC910 ct_fifo packet:
status | The claim class in one string: module_local_visible_output_equivalence_packet. It names the boundary of the claim, not a marketing word. |
customer_ready | A boolean the packet declares about itself. ct_fifo ships false even though its proof legs close. A receipt that can say no about itself is the point. |
known_boundaries | Scope limits, in the packet, as data. Limits travel with the result they bound. |
artifact_hashes | Every cited file is hash-pinned. Change a byte in a log or netlist and the packet no longer verifies. This is what the public verifier checks. |
proof_receipts | Pointers from each claim to the exact pinned log that backs it, so a number is never more than one hop from the tool output that produced it. |
toolchain | The pinned suite the packet was measured with, so a replay uses what produced the numbers. |
what formal proof output looks like
Quoted byte-for-byte from the pinned logs. Each carries its scope; none is a whole-core, ISA, or signoff claim.
SAT proof finished - no model found: SUCCESS!Induction step proven: SUCCESS!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. What a packet cannot prove, it says.
05cli reference
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.
first run and diagnostics
kairos quickstart | First-time onboarding flow: detects the environment, checks engines and configuration, runs doctor, then verifies a bundled RTL sample. |
kairos setup | Configures Kairos for the current seat. --check validates without changes; --user-install places engines under ~/.local/bin. |
kairos doctor | Checks license, model routing, local proof/EDA tools, telemetry routing, and update status. --verification-only · --deep · --strict · --json. |
kairos eval-license | Writes an evaluation-license payload for trial setup. Production trials are signed by Athanor. |
verification and optimization
kairos verify | Verifies an RTL design, formal proof source, certificate bundle, or design-closure directory. Text output reports the scoped verdict and next action; --json emits the same envelope. |
kairos verify-change | Adjudicates an optimization receipt package or a gold/candidate RTL pair. --negative-control proves the gate can fail; --run-replay before relying on the package. |
kairos optimize | Proposes and checks RTL optimization candidates. --plan-only and --estimate-only do not execute; --out writes a durable run directory. |
kairos certify-customer | Checks a <block>_kairos_cert.tar.gz package: artifact integrity, claim taxonomy, and whether it is customer-promotable. |
kairos repair | Diagnoses and repairs RTL or repository issues. --review for diagnose-only, --fix to apply, --dry-run for previews. |
benchmark and integration
kairos benchmarks list | Lists the shipped open-source silicon benchmark catalog with claim boundary and docs pointer per case. |
kairos benchmarks show | Prints one case and the exact copy-pasteable command with fixture paths resolved. |
kairos mcp serve | Starts the stdio MCP server for Claude Code, Cursor, Cline, OpenHands, and supported IDE agents. |
kairos mcp install | Auto-detects a supported IDE and installs Kairos as an MCP server. --target forces one. |
06script integration
import subprocess, json
result = subprocess.run(
["kairos", "verify", "arbiter.sv", "--json"],
capture_output=True, text=True,
)
verdict = json.loads(result.stdout)
print(verdict["status"]) # scoped result status
print(verdict["detail"]) # per-property breakdown07requirements
- Customer-provisioned Kairos image or private package
- License material and any configured model provider credentials supplied through the customer's approved environment
- RTL verification toolchain included in licensed customer images
- Linux or macOS (Windows via WSL2)
Read about security, data handling, and IP protection on the trust page.
your designs stay yours.
Customer RTL never leaves your infrastructure unless you choose to share it. What your security team needs, on one page.
Local-only mode
--local-only disables all trace upload and telemetry. Designs stay on your machine.
Air-gapped operation
KAIROS_OFFLINE=1 disables LLM network preflight. Pair with a local backend for fully air-gapped verification.
No training
Customer code and designs are never used to train or fine-tune models.
Signed licenses
License verification via GPG signature validation. Forged licenses are rejected.
Isolated certificates
Certificate generation is structurally isolated from LLM-influenced code paths.
Injection checks
Prompt-injection checks on model-facing text paths; file-accepting integrations enforce containment and reject traversal.
Compiled distribution
Strategy-rich modules ship as compiled binaries, not readable source.
Optional traces
Trace upload is disabled with --local-only or KAIROS_NO_TRACE=1.
Local certificates
Generated locally, with artifact hashes and provenance.
Your keys
All API keys and tokens live in customer-controlled infrastructure. Private images are provisioned during onboarding.
Provisioned access
A licensed image or private package per customer environment. The public athanor-sdk PyPI package is not the current channel.
License state
kairos doctor reports whether a license is missing, expired, or ready.
The checker generates the certificate. The model does not.
Share deployment details with your Athanor contact to start enterprise licensing or plan a custom deployment.