Turning rulebooks into verified tools
We had AI agents turn three rulebooks (NBA transactions, US income tax, airline baggage fees) into Lean functions with proved properties, reframing each rulebook as a formal specification. LLMs then call the verified functions as deterministic tools, scoring 90.7–100% where unaided models fall as low as 9%, every verdict traceable to its rules.
15th July 2026
Migrating Code by Proof: From F# to Python
We built a deterministic, LLM-free translator from Python and F# into Lean, reframing code migration as a proof obligation. Our automated prover then shows an F# algorithm and its Python rewrite compute the same function on every input, producing a ~22,000-character machine-checked proof.
6th July 2026
Logos Research launches to make AI reasoning trustworthy in high-stakes environments↗
Imperial College London covers our launch from stealth, with perspectives from Prof. Kevin Buzzard, Prof. Johannes Muhle-Karbe, and our investors.
26th May 2026
Stress-testing Logos formalisation platform on graduate-level probability and stochastic analysis
Findings from 18 experiments by Prof. Massimiliano Gubinelli, producing 144,000 lines of machine-checked Lean across 2,248 verified items.
22nd May 2026
Logos achieves state-of-the-art 99.4% on verified code synthesis benchmark
Our system reaches a state-of-the-art 99.4% on Verina, a benchmark for code synthesis with formal, machine-checked proofs of correctness.
7th May 2026
Why formal verification is the missing infrastructure layer for AI agents↗
Our CEO Cristopher Salvi discusses with SOSV partners Po Bronson and Parikshit Sharma why verified code is the answer to unreliable AI output.
27th April 2026