Product
Tau
Provably correct code,
down to the binary.
Ship critical software with a mathematical proof of correctness. Tau hands you an audit-ready certificate that your binary behaves exactly as intended on every possible input, regardless of who or what wrote the code.
What we offer
Tau, end to end.
Tau analyzes your compiled binary at the instruction level, captures your intent as a human-readable spec, and proves the binary safely honors the spec on every possible input, returning a kernel-signed certificate of correctness ready for auditors and regulators.
Your code
Source code in Rust, C++, or 30+ other languages.
Tau
Tau reasons about your code and proves the binary honors the spec.
Certificate of correctness
A kernel-signed certificate for auditing, or a precise bug report.
Tau runs on Talos, our open-source Lean-formalized Wasm interpreter. Free to use under a permissive license. The proof construction and enterprise support come standard with Tau.
The case for proof
Why this matters more than ever.
AI systems can now find and exploit flaws that human reviewers miss[1]; they also write code at a complexity beyond human comprehension and a pace increasingly beyond human capacity to audit[2].
Vulnerabilities, by year
Across all bug classes; CVE-disclosed.
Disclosed vulnerabilities per year, across all bug classes. 2020 and 2024 per NVD CVE catalog and Mandiant[8]. 2026 onward estimated; proxied by the accessibility of AI vulnerability-research tools to a widening set of actors[1].
The gap of unit testing
For a function on two 64-bit integers.
The tested bar is invisible at this scale (10²² × smaller than an atom). At one billion tests per second, covering every input takes 100 billion times the age of the universe.
Only mathematical proof scales with this threat. Tau is built around that premise.
Working at the binary level keeps Tau grounded in what the machine actually runs, not what you wrote in source. It also keeps the approach language-agnostic and future-proof, regardless of how your stack evolves.
Technology
How Tau proves what it claims.
Tau, Talos, and the Wasm binary all run inside Lean: one trusted proof system, end to end. There is no separate execution model that could disagree with the binary, no second prover whose soundness you need to take on faith. Trust collapses to a single program: the Lean kernel.
Our stack
See it in action
From source to certificate.
Hand Tau a Rust function. It produces a Lean theorem the kernel verifies. Below: the whole pipeline, on one real example.
▎ the compiled function matches the textbook gcd, on every input
The example
Stein's binary GCD, the greatest-common-divisor routine that ships in the num-integer crate. Production Rust, taken verbatim.
What this guarantees
On every pair of 64-bit unsigned integers, the compiled function returns the mathematical gcd. Every input. Not just the ones in the test suite.
Use Tau
Verify your code now.
Mission-critical software.
Tau is built for software whose failure has direct financial, security, or regulatory consequences: finance, cryptography, energy, and supply chain.
Talk to us.
We work with engineering teams in finance, security, and infrastructure to certify the systems that have to be right.
References