Holistic specifications for robust code

on YouTube ↗43m

" summary

Claims a new specification language — holistic specifications — that expresses necessary (not just sufficient) robustness conditions using spatial, temporal and authority predicates. It gives formal semantics (modules, configurations, linking) and mechanized assertions like access and authority, change and future, and an external/domination condition. Applied to ERC‑20, the DAO reentrancy bug and DOM wrappers, the specs show how to prove balances won’t vanish and wrappers limit reach, and they scale by quantifying over all linked modules in an open‑world model.

AI-written summary · about

" chapters (9)

1. 0:00Start
2. 12:47ERC20 classical spec
3. 16:44holistic spec - authority
4. 18:42DAO simplified
5. 23:40Example 3: DOM attenuation
6. 31:18using holistic spec
7. 35:15Semantics of Expressions
8. 35:46Semantics of holistic Assertions
9. 40:52Summary of our Proposal

" related talks

• 31mNecessity Specifications for RobustnessSophia Drossopoulou, Julian Mackay, James Noble, Susan Eisenbach · OOPSLA 2022
• 23mSpecifying and Verifying Future ConditionsWei-Ngan Chin, Yahui Song, Darius Foo · SAS 2025
• 22mThe New CodeSean Grove · AI Engineer World's Fair 2025
• 31mCooperative Specification via Composition ControlL. Thomas van Binsbergen, Christopher A. Esterhuyse · SLE 2024
• 22mA Categorical Basis for Robust Program AnalysisZachary Kincaid, Shaowei Zhu · PLDI 2026
• 17mReasoning about External CallsSophia Drossopoulou, Julian Mackay, James Noble, Susan Eisenbach · OOPSLA 2025
• 19mSynthesizing SpecificationsKanghee Park, Loris D'Antoni, Thomas Reps · OOPSLA 2023
• 28mGradual Verification: Assuring Software IncrementallyJonathan Aldrich · IWACO 2025