Skip to content
This repository has been archived by the owner on Sep 11, 2024. It is now read-only.

Commit

Permalink
Typos fixed
Browse files Browse the repository at this point in the history
  • Loading branch information
Mr-HoDL58 authored Oct 26, 2023
1 parent 42b4c85 commit 871a815
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions website/learn/consensus/specification/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ title: Consensus specification
sidebar: Specification
---

# Consensus specification
# Consensus Specification

Developing distributed and concurrent systems is a complex task that requires careful attention to the details.
Testing such systems is challenging because it's difficult to simulate all possible states,
Expand All @@ -26,20 +26,20 @@ expensive to correct in code.

To know more about TLA+, check [The TLA+ Home Page](https://lamport.azurewebsites.net/tla/tla.html).

## Pactus consensus spec
## Pactus Consensus Spec

Pactus [consensus specification](https://github.com/pactus-project/pactus/tree/main/consensus/spec)
has written in TLA+ format. It includes all invariants that can be held
in every state of every execution that the protocol allows. The TLA+ specification is compiled into
[PDF file](https://raw.githubusercontent.com/pactus-project/pactus/main/consensus/spec/Pactus.pdf).

### Safety proof
### Safety Proof

By defining some invariants we can ensure the safety of the consensus
[protocol]({{ site.baseurl }}/learn/consensus/protocol) in any possible and
distinct state, and therefore we have the informal safety proof of the Pactus consensus protocol using TLA+.

### Liveness proof
### Liveness Proof

Checking the liveness is not easy, but with defining some constraints, we have the informal proof of
liveness of Pactus consensus protocol using TLA+.

0 comments on commit 871a815

Please sign in to comment.