Assume-Guarantee Reasoning¶

Why It Matters¶

You can't verify a component in isolation without knowing something about its context. But you also can't verify it against all possible contexts. Assume-guarantee gives you the middle ground: explicitly state environmental assumptions, then prove guarantees under those assumptions. This makes verification tractable while keeping it honest about dependencies.

The Key Move¶

For any component, explicitly list assumptions about its environment (inputs, other components, timing, resources). Then specify guarantees - what it promises given those assumptions. Verify the implication: assumptions → guarantees. When composing, check that each component's assumptions are met by the guarantees of what it depends on.

Classic Application¶

Concurrent algorithm verification. To verify a lock-free algorithm, assume:

1. atomic operations are truly atomic,
2. memory is sequentially consistent,
3. threads don't fail mid-operation. Under these assumptions, guarantee:
4. operations are linearizable,
5. progress is wait-free. Both assumptions and guarantees are explicit and checkable.

Surprising Application¶

Delegation effectiveness. When delegating, be explicit about assumptions: "I assume you have context on the project, can access the database, and have 3 hours." And guarantees: "I guarantee the report will be accurate, formatted per the template, and ready by Friday." Both parties can verify assumptions hold and assess if guarantees were met.

Failure Modes¶

Hidden assumptions - assuming things without stating them, breaking verification when they're violated. Unrealistic assumptions - assuming conditions that never actually hold. Weak guarantees - promising so little the verification is vacuous. Assumption-guarantee mismatch - component A's guarantees don't satisfy component B's assumptions.

Go Deeper¶

Pnueli, "In Transition from Global to Modular Temporal Reasoning about Programs" (1985); McMillan, "Circular Compositional Reasoning about Liveness" (1999)