This work demonstrates how highly automated theorem proving can be leveraged for sparing testing costs during certification of safety-critical software such as in avionics. A verification framework for distributed interactive systems is presented. Components are modeled as stream processing functions. The functional methodology is modular with respect to serial, parallel and feedback composition. To specify and formally verify properties of distributed systems, a stream-based verification infrastructure is encoded in the theorem prover Isabelle. Composition operators for components are provided, thus allowing to scale proofs from individual components to complex networks. The underlying mathematical theory FOCUS stands out among competitors by the fact that refinement is fully compositional. The associativity and commutativity of the provided general composition operator enables a compositional verication. In this paper the stream theory encoded in Isabelle is demonstrated. This represents a small part of our encoding of the methodology focusing only on channel histories specications, yet sufficient to demonstrate dealing successfully with underspecification, supporting automatic refinement checking during design time, time-sensitive specication, as well as verifying safety and liveness properties. The theory is evaluated in a case study where the occurring refinement steps from system requirements, to high level requirements, to low level requirements, until an implementation is reached, are demonstrated to be proven correct at the push of a button.