Software verification typically assumes a “closed world”: that all modules of a system can be verified, or at least the provenance of all the modules can be assured. Real systems, however, have to interact with the “open world”: third or fourth party components, or whole external systems, with unknown provenance and assurance. Components’ interfaces may be specified, but a verified system would be unwise to trust such components unreservedly.