Updates

• Transformative AI is here. Now what?September 1, 2026

  Our thesis: why formal verification is the infrastructure AI needs, and why software is next.

• Organizing Mathematical Knowledge in the Age of AI and FormalizationJuly 20, 2026

  Two days at the National Academies in Washington, DC. The problem is no longer proving. It is digesting the proofs.

• Tau-prover v1July 13, 2026

  We came third in the hardest benchmark in the world, ahead of every frontier model.

• FMxAI 2026June 1, 2026

  Back at SRI, eight months later. We shared Talos with leading formal verification experts from around the world, and began collaborations to accelerate software verification in Lean.

• TalosMay 20, 2026

  An open-source interpreter that lifts compiled binaries into a form that can be reasoned about formally.

• Mathematics, AI, and Formalization: The State of PlayMarch 20, 2026

  A brief history of computer-aided mathematics.

• FMxAI 2025September 30, 2025

  Formal methods meets AI at SRI. Proving is still a bottleneck.