/whipstaff

A specification of the CBC Casper consensus protocols written in TLA+ and PlusCal (transpiled to TLA+)

Primary LanguageTLA

Whipstaff

A specification of the CBC Casper consensus protocols written in TLA+ and PlusCal (transpiled to TLA+). Currently using one member of this family of protocols, the binary consensus protocol, as an example.

Implementation Notes

  • Message authentication is not included in this specification due to the assumption that the validators can verify the authenticity and source of messages
  • This specification has the assumption that all messages are being successfully sent and received without time delay.
  • In this specification, equivocating validators take different subsets of all messages received, use the subsets to obtain and estimate, and send different messages to different validators.
  • The validator weights and byzantine threshold can be real numbers but they are specified as integers in this specification.
  • A temporal property check_safety_with_oracle checks whether finality has been reached by checking for the existence of an e-clique with a clique oracle.

How To Run This?

  1. Obtain The TLA Toolbox

  2. Open the .tla file in the toolbox and build a model

  3. Select the desired invariants and properties to check in 'Model Overview'

  4. Specify the values of the constants

    • validators: a range of integers from 1 to N (number of validators), inclusive

    • consensus_values: a range of integers from 0 to 1, inclusive (for a binary consensus protocol)

    • defaultInitValue: [ model value ]

    • validator_weights: a tuple of length N specifying the weight of each validator, which are integers

    • validator_initial_values: a tuple of length N specifying the initial estimate of each validator when no messages have been received

    • byzantine_threshold: an integer less than the sum of the weight of all the validators

    • byzantine_fault_nodes: a set containing the names of equivocating validators

    • message_ids: an integer specifying the maximum number of messages sent

      Example:

      validators <- 1..3
consensus_values <- 0..1
defaultInitValue <- [ model value ]
validator_weights <- <<334, 333, 333>>
validators_initial_values <- <<1, 0, 1>>
byzantine_threshold <- 334
byzantine_fault_nodes <- {1}
message_ids <- 8

Results

Finality cannot be reached when more than one-third of the validators by weight are equivocating.