Introducing TauNewThe fastest binaries, proved correct.→Tau is live
Reliable speedups for large workloads
Tau optimizes the routines that use most of your compute for your data and your machines, and proves in Lean that each version behaves exactly like the original.
Latest
- Introducing TauPinned
Production code, faster than the best implementations available, and proved correct down to the binary.
- Transformative AI is here. Now what?Pinned
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.