We are back at SRI International for the second Formal Methods × AI, June 1 to 3. The room has grown from about fifty to about eighty, with backing from Coefficient Giving, Halcyon Futures, Harmonic and ARIA. Invitees included Keri Warr of Anthropic, Buck Shlegeris of Redwood Research, Nora Ammann of ARIA and Tom Kalil of Renaissance Philanthropy.
Talos had been open source for two weeks. It is our interpreter, written in Lean, that lifts compiled binaries into a form a prover can reason about, so correctness can be proven on the code that actually runs rather than on the source.