  We present a novel mathematical framework for the specification and analysis
of fault-resilient distributed protocols and their implementations, with the
following components: 1. Transition systems that allow the specification and
analysis of computations with safety and liveness faults and their fault
resilience. 2. Notions of safe, live and complete implementations among
transition systems and their composition, with which the correctness (safety
and liveness) and completeness of a protocol stack as a whole follows from each
protocol implementing correctly and completely the protocol above it in the
stack. 3. Applying the notion of monotonicity, pertinent to histories of
distributed computing systems, to ease the specification and proof of
correctness of implementations among distributed computing systems. 4.
Multiagent transition systems, further characterized as centralized/distributed
and synchronous/asynchronous; safety and liveness fault-resilience of
implementations among them and their composition. The framework is being
employed in the specification of a grassroots ordering consensus protocol
stack, with a grassroots dissemination protocol and its implementation of
grassroots social networking and of sovereign cryptocurrencies, and an
efficient Byzantine atomic broadcast protocols as initial applications.
