Transformative AI is here. Now what?

Every transformative technology needed infrastructure to become exponential. The grid for electricity. CUDA for GPUs. AI needs its own, and its core is formal verification. And we are building that infrastructure.

Mathematics has already validated it. Mathlib, a library of formally verified knowledge built over years, is what lets models operate at the frontier of the field: this year they settled the Jacobian conjecture, open since 1939, and improved century-old bounds related to the Riemann hypothesis. Fermat’s Last Theorem - often cited as one of humanity’s greatest achievements - was recently autoformalized in a matter of days, outpacing collaborative human efforts that have been ongoing for years.

Software is next, and the stakes are higher. The same proofs for mathematical theorems can also prove software correct. Most production code is increasingly written by machines, faster than humans can review or test. At the same time, frontier AI is becoming increasingly capable of finding and exploiting vulnerabilities. Under these conditions, proving correctness is now imperative.

As proofs hold for every input and are machine-checkable, correctness no longer depends on a human reading and reviewing code. And proven results never need to be checked again, so knowledge can compound - allowing us to build and control arbitrarily complex systems whose output exceeds human comprehension.

Just as Mathlib exponentiated math, we are building the infrastructure to exponentiate software. We are starting with one of the holy grails of computer science: verifying code down to the binary. And that is just one part of a larger infrastructure we are building.

It’s an exciting time to be alive.

Get in touch, or join the team.