TL;DR: Formal verification uses mathematical proofs to guarantee a system behaves as intended.  Cajal is massively scaling this technology with AI - deploying agents to autonomously discover and formalize new tools across applied mathematics with genuine real world impact. Starting with quantum computing and finance.

https://www.youtube.com/watch?v=7McsRwyWBNE

LLMs: The State of Play

Large language models are fundamentally stochastic. No amount of scaling changes this - probabilistic systems cannot guarantee correctness. This is especially problematic in mission-critical domains that require mathematical certainty.

Formal verification provides exactly this: mathematical proof that code is correct for every possible input, not just the ones you test.

Previously, this technology has been limited to a small group of experts working over long horizons - restricting its application to narrow domains like software verification and research mathematics.

A New Frontier for Formal Verification

Cajal is using AI to massively scale this technology - deploying agents to autonomously discover and formalize tools across applied science, beginning with quantum computing and finance.

Introducing Tau: Tau is a multi-agent system that collaborates to discover and verify new mathematical proofs in Lean. Given a research direction, Tau autonomously formalizes large corpora of applied mathematics, discovering novel results with real-world applications - from algorithms with certified speedups to certificates that a system satisfies its constraints.

Every result is machine-verified by Lean's type-checking kernel, guaranteeing correctness.

Our Ask
Alongside our work formalizing applied mathematics, we also partner with frontier AI labs and research institutes to improve their systems, including through datasets, evals, and RL environments. To explore a collaboration, contact us at hi@caj.al.

→ Luke and Pedro from Cajal

Back in our first office in a castle in Germany, where it all began (long story!)