Formal verification tool that proves compiled software is correct down to the machine level.
Tau works directly on compiled binaries, captures the developer's intent as formal specifications, and proves them mathematically — returning either an audit-ready certificate of correctness or a bug report listing what breaks them. It is built on Talos, an open-source interpreter that lifts binaries into a form suitable for formal reasoning. Cajal positions this as essential infrastructure for an era where AI writes code faster than humans can audit it. Tau is a product of Cajal.