Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML

Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

Research output: Contribution to journalArticlepeer-review

11 Citations (Scopus)


Distributed programs are known to be extremely difficult to implement, test, verify, and maintain. This is due in part to the large number of possible unforeseen interactions among components, and to the difficulty of precisely specifying what the programs should accomplish in a formal language that is intuitively clear to the programmers. We discuss here a methodology that has proven itself in building a state of the art implementation of Multi-Paxos and other distributed protocols used in a deployed database system. This article focuses on the basic ideas of formal EventML programming illustrated by implementing a fault-tolerant consensus protocol and showing how we prove its safety properties with the Nuprl proof assistant.
Original languageEnglish
Number of pages15
JournalElectronic Communications of the EASST
Publication statusPublished - 2015
Event15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015) - Edinburgh, United Kingdom
Duration: 1 Sept 20154 Sept 2015


  • functional programming
  • formal methods
  • formal verification
  • theorem proving
  • distributed systems
  • fault tolerance
  • event logic
  • event-based programming


Dive into the research topics of 'Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML'. Together they form a unique fingerprint.

Cite this