TLA+ is a formal modeling language for algorithms running in a distributed system.
It would be interesting to create animations and sequence diagrams from modeling languages so that users could get an intuitive understanding of the protocols being modeled.