  Distributed systems are critical to reliable and scalable computing; however,
they are complicated in nature and prone to bugs. To modularly manage this
complexity, network middleware has been traditionally built in layered stacks
of components. We present a novel approach to compositional verification of
distributed stacks to verify each component based on only the specification of
lower components. We present TLC (Temporal Logic of Components), a novel
temporal program logic that offers intuitive inference rules for verification
of both safety and liveness properties of functional implementations of
distributed components. To support compositional reasoning, we define a novel
transformation on the assertion language that lowers the specification of a
component to be used as a subcomponent. We prove the soundness of TLC and the
lowering transformation with respect to the operational semantics for stacks of
distributed components. We successfully apply TLC to compose and verify a stack
of fundamental distributed components.
