In today’s complex software, internal, trusted, code is tightly intertwined with external, untrusted, code. By definition, internal code does not trust external code. From an internal perspective, the effects of outgoing calls to external code – external calls — are necessarily unknown and unlimited.

Nevertheless, the effects of external calls can be tamed if internal code is programmed defensively, i.e. to ensure particular effects cannot happen. Tamed effects allow us to prove that internal code preserves assertions about internal and external objects, even in the presence of outgoing calls and callbacks.

This paper addresses the specification and verification of internal code that makes external calls, using encapsulation and object capabilities to tame effects. We propose new assertions for access to capabilities, new specifications for tamed effects, and a Hoare logic to verify that a module satisfies its tamed effects specification, even while making external calls. We illustrate the approach though a running example with mechanised proofs, and prove soundness of the Hoare logic.