Velisarios: Byzantine fault-tolerant protocols powered by coq

Vincent Rahli, Ivana Vukotic, Marcus Völp, Paulo Esteves-Verissimo

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Scopus citations


Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these systems. Byzantine fault-tolerant state-machine replication (BFT-SMR) provides a way to harden such systems. It ensures that they maintain correctness and availability in an application-agnostic way, provided that the replication protocol is correct and at least n- f out of n replicas survive arbitrary faults. This paper presents Velisarios, a logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols. As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT.
Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer [email protected]
Number of pages32
ISBN (Print)9783319898834
StatePublished - Jan 1 2018
Externally publishedYes

Bibliographical note

Generated from Scopus record by KAUST IRTS on 2021-03-16


Dive into the research topics of 'Velisarios: Byzantine fault-tolerant protocols powered by coq'. Together they form a unique fingerprint.

Cite this