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