Blog
Proving a CUDA kernel matches its PyTorch specification
We give PyTorch programs and CUDA kernels a shared denotational semantics in Lean, so the two can be compared as mathematical objects rather than by sampling outputs. Both translations are deterministic compilers, and every verdict is a machine-checked proof or a computed counterexample. The first divergences we found were in ReLU.
26th August 2026
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
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