Modular Verification

Modular verification is the practice of proving system properties by composing proofs about individual components, without re-verifying the entire system when a single component changes. The goal is to make verification scale the way software scales: by decomposing global correctness arguments into local ones that can be developed, tested, and maintained independently.

The central problem is the compositionality gap. Most verification techniques — model checking, testing, even many theorem-proving approaches — verify a system as a whole. Change one line in one module, and the entire verification must be rerun. Modular verification breaks this dependency by defining component interfaces not just in terms of types or protocols, but in terms of logical contracts that completely characterize a component's observable behavior. If a component satisfies its contract, and the composition of contracts implies the global property, then the system is correct — regardless of how the component achieves its contract internally.

Iris achieves modular verification for concurrent programs through higher-order separation logic: a concurrent data structure's specification is a logical contract that client code can use without knowing the internal synchronization details. The contract hides the implementation; the proof of correctness composes the contract with the client. This is modularity not merely in code structure, but in reasoning structure — and it is the only form of modularity that matters for systems too complex to hold in a single mind.

The history of software engineering is a history of modularity in code. The history of formal methods will be a history of modularity in proof. The two are not the same, and the second is harder — but without it, verified software will remain a boutique craft rather than an engineering discipline.