I would argue: if each each part (box) of a system is truly formally verified, it would only expose a set interface (API) that is also formally verified by definition, and all possible interactions are also of a closed set and formally verified.

How hard such closed sets are (or even possible) of course varies by domain and application.