Group communication system assist the development of fault-tolerant distributed algorithms by providing precise guarantees on message ordering, delivery, and synchronization. Ensemble is a widely used group communication system that is highly modular and configurable. Formally verifying Ensemble is a formidable task, but it has wide-ranging benefits, from formal assistance in the design of new distributed applications, to ensuring the reliability of critical distributed algorithms for all applications that use Ensemble.
In this paper, we present a verification framework that we are using the verify Ensemble in the Nuprl proof development system. The framework is based on I/O automata, which are ideal for the verification in some respects: they they specify modular components that range from concrete protocol code to abstract services. But traditional I/O automata do not allow re-use of formal theorems as automata are composed. We present a new type-theoretic basis for I/O automata that preserves safety properties during composition using an object-oriented methodology.