Athanor AI

Athanor AI develops verification infrastructure intended to decide whether AI-generated designs, programs and proofs are correct. Its first system, Kairos, is described as a verification engine for hardware and software that takes a stated claim — equivalence, safety, or a bound — and returns one of three verdicts: proved, refuted, or inconclusive. Accepted results ship with an artifact that justifies them: a replayable proof term (for example an equivalence proof, an induction certificate, or a Lean 4 proof term), or, for refutations, a concrete counterexample such as the exact input sequence or state that breaks the claim. Each verdict carries a receipt pinning tool versions, assumptions, scope, synthesis recipe and other measurement conditions needed to reproduce the result, plus an explicit statement of what the packet cannot prove.

The workflow positions a model as a proposer and the checker as the authority: AI drafts a candidate, proof or optimization, and Kairos orchestrates bounded model checking, temporal induction and Lean 4 obligations until the claim closes or fails. Malformed specifications are rejected at intake. In optimization mode the same loop applies — each candidate RTL variant must be proved equivalent and show a measured area reduction from synthesis tools, and a packet whose metric screen fails is refused (marked customer_ready: false) even when its proof legs close. Stated policies include never promoting inconclusive results, never labelling statistical testing as formal proof, and disclosing verification method on certificate labels. The engine exposes commands including verify, optimize, verify-change, repair, doctor and an MCP server mode, and cites backends such as EBMC, Lean 4 and SBY/ABC.

Athanor also publishes public demonstration packets built on open RISC-V designs, including ibex_fetch_fifo (promoted: lower cell counts under recorded flows, bounded sequential checks, temporal induction, an independent SBY/ABC PDR leg), ct_fifo (refused because timing regresses) and ct_pmp_top (gap: same-state proof reproduced byte-exact by a non-author, with PPA, timing and toggle legs unavailable). Its GitHub organization hosts an open-source Lean 4 tactic library (pythia), telos (a DSL compiling one congestion-control spec into Lean 4, Dafny, EBMC, Hypothesis and CPU-sim cross-checks), kairos-cedar (synthesizing Cedar policies from a Lean formalization to differentially test production Cedar implementations), replication packages for academic submissions, and Athanor-optimized forks of RISC-V cores including Ibex, CV32E40P, OpenC910 and riscv-boom.

Business model

Kairos is licensed per customer environment rather than distributed publicly: customers share deployment details, then receive a private image or package, credentials and a runbook provisioned for their environment, with evaluation access issued during onboarding. Enterprise access is requested through the website.

Per-customer environment licensing of the Kairos image, with evaluation access granted during onboarding.

Traction

The website lists institutional collaborations with Carnegie Mellon University, the University of Pennsylvania and Seattle Children's Hospital, and publishes recorded engine runs including a seven-assertion arbiter lock proof discharged in 0.278 seconds and a machine-checked refutation of BBRv3 starvation-onset bounds closed by five independent verifiers from a 78-line specification. The GitHub organization lists 17 repositories, including replication packages for NeurIPS 2026 and AI4Math @ ICML 2026 submissions; the pythia tactic library has 17 stars.

Latest developments

Publications dated April 2026 cover a machine-checked refutation of BBRv3 starvation, an end-to-end hardware solve walkthrough (fix_arb_lock), an assessment of whether a formal-verification layer improves kernel quality, and formal verification of dopamine reward prediction. GitHub activity through August 2026 includes Athanor-optimized forks of the CV32E40P, Ibex, OpenC910 and riscv-boom cores and replication packages for NeurIPS 2026 and AI4Math @ ICML 2026 papers.