PV4 Consensus Verifiertranslates a consensus algorithm into a PROMELA model and LTL properties

Model checking tool for consensus algorithms formulated in the ConsL language

Application domain/field

Type of tool

Specification/model translator?

Expected input

Consensus algorithm


ConsL (own) language

Expected output

PROMELA/Spin model


The tool automatically translates a ConsL algorithm into appropriate PROMELA models and LTL properties for the SPIN model checker.
Model checking


Project page: http://www.infsec.ethz.ch/research/software/consl-verifier

Related papers

https://doi.org/10.1007/978-3-319-63390-9_12 (CAV '17)

Last publication date

13 July 2017

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.