Skip to content

feat(FLP): define pseudo-consensus and prove that it is implied by consensus#718

Open
ctchou wants to merge 2 commits into
leanprover:mainfrom
ctchou:flp-pseudo
Open

feat(FLP): define pseudo-consensus and prove that it is implied by consensus#718
ctchou wants to merge 2 commits into
leanprover:mainfrom
ctchou:flp-pseudo

Conversation

@ctchou

@ctchou ctchou commented Jul 13, 2026

Copy link
Copy Markdown
Collaborator

This PR defines the notion of a fault-tolerant "pseudo-consensus" algorithm, which is central to Völzer's proof, and proves that every f-tolerant consensus algorithm is also a f-tolerant pseudo-consensus algorithm. This resilt is intuitively obvious and is stated without proof in Völzer's paper, but it turns out to require quite a bit of formal machinery (given in FairSchedular.ean) to prove.

Zulip discussion: #CSLib > Impossibility of distributed consensus

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant