Athanor
Proving or disproving computational claims, end to end.
We build Kairos, an agent-orchestrated verification engine that proves or disproves claims in computational science and engineering with upper and lower bounds. 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
Bounds, not vibes.
Kairos takes a hypothesis and returns bounds on it. The engine composes specialized agents, each responsible for one verification modality, and returns a machine-checkable artifact: a Lean proof, a property-test corpus, a simulation sweep, or a sandwich bound combining all three. Every handoff between agents is gated by the verifier native to that layer, so what reaches the final report has already been independently checked.
01
Orchestrated
A multi-agent fleet routes each hypothesis through domain encoding, formalization, property testing, and paradigm replay, with verification-gated handoffs between stages.
02
Two-sided
For every claim Kairos returns an upper and a lower bound, theoretical, empirical, or both, rather than a single pass/fail score.
03
Agentic
Agents resume across sessions, accumulate partial progress on hard theorems, and close proof obligations that exceed a single model's working context.
Applications
Where Kairos has been applied.
One stack, three domains: the scientific and engineering claims Kairos has closed so far group into life sciences, hardware verification, and software systems.
Life sciences
Neuroscience convergence theorems
Kairos refutes a 25-year-old dopamine-learning convergence theorem against the Tang 2024 credit-assignment paradigm, supplies the corrected statement machine-checked in Lean 4, and sandwich-bounds the empirical time constant against four competing candidate rules.
Hardware verification
RTL correctness and accelerator kernels
SystemVerilog repair and assertion synthesis closed by EBMC bounded model-checking, paired with Lean 4 theorems for universally-quantified obligations. The same pipeline catches silently-wrong AI-generated NKI accelerator kernels that pass seeded property tests.
Software systems
Authorization policy and network protocols
Cedar authorization policies adversarially audited and proved sound in Lean 4. A closed-form sandwich bound on BBRv3 starvation cross-checked by five independent backends, with a patched filter certified against the complementary positive theorem.