• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
        • Aleobft
          • Aleobft-static
          • Aleobft-stake2
          • Aleobft-dynamic
            • Correctness
              • Unequivocal-accepted-certificates-def-and-init
              • Signer-records
              • Same-committees-def-and-implied
              • Dag-omni-paths
              • Unequivocal-accepted-certificates-next
              • Unequivocal-signed-certificates
              • Nonforking-anchors-def-and-init-and-next
              • Signer-quorum
              • Quorum-intersection
              • Successor-predecessor-intersection
              • Same-owned-certificates
              • Previous-quorum
              • Last-anchor-voters-def-and-init-and-next
              • Certificates-of-validators
              • Committed-redundant-def-and-init-and-next
              • Nonforking-blockchains-def-and-init
              • Fault-tolerance
                • Committee-correct-members
                • Committee-faulty-members
                • All-system-fault-tolerant-p
                • Validator-fault-tolerant-p
                • Committee-fault-tolerant-p
                • System-fault-tolerant-p
              • Rounds-in-committees
              • No-self-messages
              • Blockchain-redundant-def-and-init-and-next
              • Backward-closure
              • Accepted-certificate-committee
              • Nonforking-blockchains-next
              • Anchors-extension
              • No-self-endorsed
              • Last-anchor-present
              • Committees-in-system
              • Last-blockchain-round
              • No-self-buffer
              • Dag-certificate-next
              • Omni-paths-def-and-implied
              • Simultaneous-induction
              • Ordered-even-blocks
              • Last-anchor-def-and-init
              • Same-committees
              • Committed-anchors-sequences
              • Last-anchor-next
              • Unequivocal-accepted-certificates
              • Omni-paths
              • Last-anchor-voters
              • Committed-redundant
              • Nonforking-blockchains
              • Nonforking-anchors
              • Blockchain-redundant
            • Definition
          • Aleobft-stake
          • Aleobft-proposals
          • Library-extensions
        • Leo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Correctness

Fault-tolerance

Fault tolerance.

In typical BFT systems, including AleoBFT with static committees, the notion of fault tolerance applies to the system as a whole, based on the number of correct and faulty validators: the system is fault-tolerant if the actual number of faulty validators does not exceed f, which is calculated from the total n, as formalized in max-faulty-for-total. With dynamic committees, the notion applies to every committee that arises during the execution of the protocol. It has to be an assumption on every such committee: it cannot be checked by validators, who do not know which validator is correct vs. faulty.

Here we formalize this notion for committees, which is then used as a hypothesis for certain correctness theorems of AleoBFT.

Subtopics

Committee-correct-members
Addresses of the correct validators in a committee.
Committee-faulty-members
Addresses of the faulty validators in a committee.
All-system-fault-tolerant-p
Check if all the system states in an execution corresponding to a sequence of events are fault-tolerant.
Validator-fault-tolerant-p
Check if the active committees calculated by a validator are all fault-tolerant.
Committee-fault-tolerant-p
Check if a committee is fault-tolerant.
System-fault-tolerant-p
Check if a system state is fault-tolerant.