Cajal Launches: Scaling Formal Verification for Scientific Discovery

Cajal recently launched!

‍

^{"Accelerating scientific discovery with rigor and trust"}

‍

^{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

‍

‍Founded by Pedro Nobre & Luke Johnston

‍

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.

‍

Learn More

‍

^{Visit caj.al to learn more.}

‍

^{Alongside their work formalizing applied mathematics, they 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 the team here.}

^‍

^{Follow Cajal on LinkedIn & X.}

‍

‍