Blog
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