Polkadot and JAM Protocol Specification in Quint

This project contains models to verify some algorithms or system used in the Polkadot ecosystem.

If Sassafras determines who builds a block, and ELVES mathematically guarantees how the block's execution is verified, BEEFY is the protocol that allows Polkadot to securely export this finality to external blockchains (like Ethereum via Snowbridge).

1. Sassafras
2. Elves
3. BEEFY
4. GRANDPA
5. JAM (Join-Accumulate Machine) protocol

Note: Confiture is the french word for Jam.

Installing Quint

To run the specification and tests, you'll need to install Quint (>=0.31):

npm install -g @informalsystems/quint

or on MacOS:

brew install quint

Jump into the README of the relevant directory

Sassafras

Elves

Beefy

Grandpa

Jam