Jason Gross and Rajashree Agrawal join Sophia Dew to explain formal verificationFormal verification uses precisely stated properties and logical methods to check whether a system or argument satisfies those properties. as proving that a specified program property holds for every relevant input. They distinguish generating a theorem statement, producing its proof and checking that proof, and describe why historical proof-writing costs limited verification to critical systems.
Theorem's approach keeps ordinary code and property-based testsProperty-based testing checks general rules about software behavior across many generated inputs instead of relying only on individually chosen examples. as the developer interface while placing proof assistantsA proof assistant is software for writing formal definitions and proofs while mechanically checking that each proof follows the rules of a logical system. behind the scenes. The discussion covers Jason Gross's experience with verification performance and why seemingly simple proof checks can become impractical until the underlying evaluation strategy is fixed.
Using agent sandboxesAn AI agent sandbox is an isolated execution environment that limits which files, processes, networks, credentials, and external systems an agent can access. as an example, the guests show how proof attempts expose both coding bugs and design weaknesses, including authentication channels that might allow access outside a sandbox. They discuss preserving useful behavior when automatically patching those systems, token-efficiency constraints and the potential role of verified environments and graders in reducing reward hackingReward hacking occurs when a system improves a measured reward or score without achieving the intended underlying goal.. These are proposed safety tools, not a claim that all current agent systems are inescapable.
Watch on YouTube
