The verification layer
for AI agents
Logos is building the mathematical infrastructure that makes AI agents logically correct over long horizons, using formal verification to ground LLM-generated code in machine-checked proofs.
Team
Cristopher Salvi
Tenured professor of mathematics and AI at Imperial. Cris’ research lies at the intersection of stochastic analysis and deep learning. He has made major contributions to generative diffusion models and post-transformer architectures for sequence modelling.
Robert Smith
Former Managing Director and Global Head of Quantitative Research in credit markets at Citi with over 20 years of experience in quantitative financial modelling. Rob built and led global teams integrating AI into advanced trading and risk infrastructure.
Massimiliano Gubinelli
Wallis Professor of mathematics at the University of Oxford. A leading figure in stochastic analysis, Max has made transformative contributions to rough path theory, singular SPDEs, and constructive quantum field theory.
Rémy Degenne
Associate professor at Inria Lille, specialising in sequential machine learning and decision theory. Rémy is a pioneer in formalising probability theory in Lean 4.
Martin Hairer
Fields Medalist, Breakthrough Prize winner, and full professor of mathematics at EPFL and Imperial. Martin's work on stochastic PDEs has reshaped modern probability and stochastic analysis.
Kevin Buzzard
Full professor of pure mathematics at Imperial and the world's leading expert in formal mathematics. Kevin is leading the formalisation of Fermat's Last Theorem, the most technically demanding project in mathematical formalisation to date.
Aitor Muguruza
Chief AI Officer at a systematic hedge fund, with a PhD in AI for financial modelling. Aitor was Risk Magazine's 2020 Rising Star award winner for his work on Deep Learning Volatility.
Maud Lemercier
Previously a postdoctoral researcher at the University of Oxford, Maud made significant contributions in high-dimensional statistics and probabilistic machine learning.
David Ledvinka
As a postdoctoral researcher in Kevin Buzzard's group at Imperial, David has made many contributions to the development of analysis and probability theory in Lean.
Mathematicians and quantitative finance leaders, now building the verification layer for AI. Plus a dedicated team of software engineers.
If you need AI agents you can trust on correctness-sensitive technical work,
get in touch.
