AnnouncementsOctober 23, 2026

Introducing Tau

Production code, faster than the best implementations available, and proved correct down to the binary.

Santiago Ramón y Cajal's drawing of a Purkinje neuron, in white on black — Purkinje neuron, drawn by Santiago Ramón y Cajal. Wikimedia Commons

Today we are introducing Tau. Tau optimizes software at the binary level, the exact machine code a processor runs, and proves that each optimized binary is correct. On some of the most widely used code in data centers, it beats the fastest implementations available.

To our knowledge, this is a first: production code made faster than the best implementations available, and proved correct in Lean down to the machine instructions, on both x86 and ARM. Previous work on formalizing machine instructions has targeted application-specific domains such as cryptography, or was limited to microcontroller architectures such as RISC-V. There have been no efforts, to our knowledge, which also extend to general production code optimization.

Here are a few of our results, to give a feel for what Tau is capable of:

Speed-up over the fastest existing buildFastest existingTau

Snappy decompression vs. Google Snappy

1.59×

PNG encoding vs. fpnge

1.38×

DEFLATE compression vs. libdeflate

1.30×

zlib decompression vs. zlib

1.20×

Figure 1. Speed-up on Intel Sapphire Rapids, each against the library's fastest build.

DEFLATE is the compression inside gzip, zip and PNG. Our compressor is 1.30× faster than libdeflate, the fastest available, with 0.3% smaller output, and 4.2× faster than zlib. Our Snappy decompressor runs 1.59× faster than Google Snappy's fastest build, and our PNG encoder 1.38× faster than fpnge.

zlib has been in use since 1995 and ships in almost every operating system. We made its decompressor 1.20× faster, and proved it behaves exactly like the original on every input. The same kind of guarantee covers each of our results: every one is a drop-in library whose binary, modeled instruction by instruction on the processor it runs on, is proved in Lean to meet its specification, or proved equivalent to the original.

How did we get here? We built proprietary formal semantics for native x86 and ARM, and the reasoning infrastructure and libraries that make optimization and proving at this scale possible. It builds on our open work: Talos, our open-source framework for reasoning about compiled WebAssembly, to appear at NeurIPS 2026.

Tau is available today, for performance optimization only. We're already working with companies whose services reach hundreds of millions of users, on the compression and media workloads that run across their fleets.

If you are running large workloads, let's chat. You can book a demo here.