Reasoning about External Calls - Specification and Verification of Internal Code with Object Capabilities

Explore a 17-minute conference presentation from OOPSLA 2025 that addresses the critical challenge of reasoning about external calls in modern software systems. Learn how researchers from Imperial College London and Victoria University of Wellington tackle the problem of verifying internal trusted code that must interact with external untrusted code, even when that external code may not be available or trustworthy. Discover new assertions for access to capabilities, specifications for limiting effects, and a novel Hoare logic designed to verify that modules satisfy their specifications while making external calls. Examine how defensive programming techniques using encapsulation and object capabilities can limit the potential effects of external calls by restricting access to necessary capabilities. Follow along with a detailed running example that includes mechanized proofs and understand the soundness proof of the proposed Hoare logic. Gain insights into program verification techniques specifically designed for today's complex software environments where internal and external code are tightly intertwined, and understand how formal methods can be applied to ensure system reliability despite dependencies on untrusted external components.