Verifying Code That Calls Code You Can't Trust • Sophia Drossopoulou • Bug Bash EU 2026

This talk presents a line of work on specifying and verifying software in open settings, where trusted internal code interacts with untrusted external code. It introduces object capabilities, protection, and scoped invariants as a way to reason about which effects external calls can cause, illustrated with a shop-account example and the Parity multi-sig failure. It then extends the approach to mediating objects through an escrow case study involving honest purses, trust, risk, and a stratified specification that resolves a paradox.