Optimizing binaries for large workloads
Tau makes the routines that use most of your compute run faster on your machines, and proves in Lean that the new binary behaves exactly like the original.
Book a demoIllustrative profile. Snappy decompression runs 1.59x faster than Google Snappy's fastest build, with identical output and no extra memory. Measured on Intel Sapphire Rapids, Silesia corpus.
How it works
Your code
A hot routine
e.g. Snappy decompression
Your data
A representative sample
e.g. logs, web assets, storage blocks
Your machine
A fixed machine type
e.g. AWS m7i or GCE C3: Sapphire Rapids, AVX-512
Tau
Optimize the routine for this data and this machine
Every candidate version is proved in Lean before it ships
You get
A faster library
Same interfaces. e.g. 1.59x faster than Google Snappy
You get
A machine-checked proof
For every input, the output is proved correct
Your code
A hot routine
e.g. Snappy decompression
Your data
A representative sample
e.g. logs, web assets, storage blocks
Your machine
A fixed machine type
e.g. AWS m7i or GCE C3: Sapphire Rapids, AVX-512
Tau
Optimize the routine for this data and this machine
Every candidate version is proved in Lean before it ships
You get
A faster library
Same interfaces. e.g. 1.59x faster than Google Snappy
You get
A machine-checked proof
For every input, the output is proved correct
Drop-in
No code changes and no migration. You swap in the faster library.
Lower compute costs
The same work on less CPU, across every machine that runs it.
Same reliability
Proved equivalent for every input, so there is nothing new to trust.