# Logos Research

> Logos Research builds the verification layer for AI: domain-specific knowledge is formalised into machine-checkable specifications, agents iterate against a theorem prover until their code is proven correct, and every artefact ships with a Logos Certificate, a machine-checked proof that it satisfies its specification.

## About

Logos Research is an AI company building infrastructure to make AI reasoning trustworthy in high-stakes environments. Our platform uses formal verification to provide machine-checked guarantees on AI-generated code and mathematical reasoning. Our first market is financial services, where model risk and governance frameworks require independent, evidence-based validation; Logos Certificates are designed to serve as that evidence, and anyone can re-check them independently of the model that produced the work. Certificates are written against FinanceLib, our growing library of formally verified financial mathematics. The same platform extends to hardware, safety-critical and scientific-computing engineering.

Founded by Cristopher Salvi (CEO) and Robert Smith (CTO), the team includes mathematicians and engineers from Imperial College London, Inria, and leading research institutions. Advisors include Fields Medallist Martin Hairer and Lean mathematician Kevin Buzzard.

Backed by Khosla Ventures, XTX Markets, and SOSV.

## Pages

- [Home](https://www.logosresearch.ai/): Landing page — mission, team, investors, and contact
- [Blog](https://www.logosresearch.ai/news/): All press coverage, research notes, and announcements

## Blog

- [Turning rulebooks into verified tools](https://www.logosresearch.ai/news/rulebooks-to-verified-tools/): On the RuleArena benchmark, a spec-writer agent formalises each real-world rulebook (NBA transactions, U.S. tax, airline fees) into Lean, proves it, and ships it as a deterministic tool the LLM calls, lifting accuracy from as low as 9% to 98–100%.
- [Migrating Code by Proof: From F# to Python](https://www.logosresearch.ai/news/migrating-code-by-proof/): A deterministic, LLM-free translator lowers Python and F# into Lean, reframing code migration as a proof obligation; our automated prover verifies that a legacy F# algorithm and its Python rewrite compute the same function on every input.
- [Logos Research launches to make AI reasoning trustworthy in high-stakes environments](https://www.logosresearch.ai/news/imperial-ai-reasoning-trustworthy/): Imperial College London covers our launch from stealth, with perspectives from Prof. Kevin Buzzard, Prof. Johannes Muhle-Karbe, and our investors.
- [Stress-testing Logos formalisation platform on graduate-level probability and stochastic analysis](https://www.logosresearch.ai/news/autoformalisation-experiments/): Findings from 18 formalisation experiments by Prof. Massimiliano Gubinelli, producing 144,000 lines of machine-checked Lean across 2,248 verified items.
- [Logos achieves state-of-the-art 99.4% on verified code synthesis benchmark](https://www.logosresearch.ai/news/verina-state-of-the-art-verified-code-synthesis/): State-of-the-art 99.4% on verified-code-generation benchmark.
- [Why formal verification is the missing infrastructure layer for AI agents](https://www.logosresearch.ai/news/sosv-is-new-math-the-answer-to-ai-slop-code/): Our CEO Cristopher Salvi recently discussed our vision with SOSV partners Po Bronson and Parikshit Sharma.

## Legal

- [Privacy Policy](https://www.logosresearch.ai/privacy-policy/)
- [Website Terms](https://www.logosresearch.ai/website-terms/)