Athanor
Proving or disproving computational claims, end to end.
We build Kairos, a multi-agent verification engine for hardware and software. For RTL optimization, LLMs propose changes and formal tools prove or refute equivalence; every accepted optimization carries machine-checked proof, measured area reduction, and reproducible conditions. Built for teams whose claims have to hold up to scrutiny, not just pass a testbench.
Academic Partnerships
Carnegie Mellon University
University of Pennsylvania
Seattle Children's Hospital
What is Kairos
Proved, not claimed.
Kairos is a multi-agent verification engine. For RTL optimization, LLMs propose changes and formal tools prove or refute equivalence. Every accepted optimization carries machine-checked proof, measured area reduction, and reproducible conditions. For theorem proving, Pythia provides the open-source Lean 4 tactic library that Kairos builds on.
01
Verified
Every accepted RTL optimization is backed by formal equivalence proof. Sequential and flop-changing accepts require independent sequential receipts.
02
Measured
Area reductions are measured by synthesis tools, not estimated by models. Certificates record the measurement conditions for reproducibility.
03
Honest
Kairos never labels testing as proof. Certificate labels disclose the verification method and confidence level. Inconclusive results stay inconclusive.
Open Source
Pythia
Pythia is our open-source Lean 4 tactic library. It provides the theorem-proving foundation that Kairos builds on: automated proof strategies, sorry closure, axiom auditing, and proof obligation tracking. Apache-2.0 licensed.
01
Tactic library
Automated proof strategies for Lean 4 including omega, bv_decide, simp chains, and custom domain-specific tactics.
02
Proof verification
Sorry closure, axiom auditing, and proof obligation tracking. Every proof is machine-checked by the Lean kernel.
Applications
Where Kairos has been applied.
Hardware verification, theorem proving, and software systems.
Hardware
RTL optimization with formal proof
Propose area-reducing RTL transformations and formally verify equivalence. Combinational and sequential designs, with measured cell reduction and reproducible conditions in every certificate.
Theorem proving
Lean 4 verification via Pythia
Machine-checked proofs in Lean 4 using
Pythia, our open-source tactic library. Sorry closure, axiom auditing, and proof obligation tracking.
Software
Authorization policy and protocol verification
Cedar authorization policy checking and congestion control protocol verification. Property-based testing, symbolic execution, and mutation testing for Python codebases.