Quint Use-Cases
Alpenglow
protocol by Anza Research
specification by Josef Widder, Yassine Boukhari, Gabriela Moreira
Formalization from the pseudo-code in the Alpenglow paper.
ChonkyBFT
protocol by Matter Labs
specification by Igor Konnov, Denis Kolegov
Specification and model checking experiments, including usage of the Twins technique.
CometBFT Gossip (Flood)
protocol by CometBFT (Informal)
specification by Hérnan Vanzetto
Literate specification for a CometBFT's gossip protocol.
CometBFT Mempool
protocol by CometBFT (Informal)
specification by Pierre Sutra, Lásaro Camargos
Formalisation & verification of the CometBFT mempool rules.
HotShot Epoch‑change
protocol by Espresso
specification by Yassine Boukhari, Josef Widder, Gabriela Moreira
Formalization of the epoch-change protocol, identifying ambiguities in the English spec.
Interchain Security
protocol by Cosmos Hub (Informal)
specification by Philip Offtermatt
Formalization and model‑based tests for Cosmos Hub's Interchain‑Security implementation.
Jellyfish Merkle Tree
protocol by Left Curve
specification by Josef Widder, Aleksandar Ignjatijevic, Gabriela Moreira
Literate specifications and model checking of Grug's Jellyfish Merkle sparse tree.
Malachite
protocol by Informal (acquired by Circle)
specification by Josef Widder, Daniel Cason
Spec & several protocol-level tests, all running on the CI for the Malachite consensus engine (powering Arc).
Minimmit
protocol by commonware
specification by Denis Kolegov, Patrick O'Grady
Formal specification for the Minimmit Byzantine Fault-Tolerant consensus protocol
MonadBFT
protocol by Category Labs
specification by Yassine Boukhari, Josef Widder, Gabriela Moreira
Formalization and witnesses for MonadBFT consensus.
Mysticeti-C
protocol by Mysten Labs
specification by Gabriela Moreira, Martin Hutle
DAG-based Consensus protocol spec, including an interactive visualization of protocol evolution.
Namada
protocol by Heliax
specification by Manuel Bravo
Fast redelegation and rewards specification with correctness properties.
Neutron DeX
protocol by Neutron
specification by Ivan Gavran, Manuel Bravo, Gabriela Moreira
Decentralized Exchange formal model.
Neutron Drop
protocol by Neutron
specification by Ivan Gavran, Aleksandar Ignjatijevic, Manuel Bravo
Liquid staking protocol specification.
Neutron Liquidity Pool Migration
protocol by Neutron
specification by Ivan Gavran, Aleksandar Ignjatijevic
Model-based testing of Neutron's liquidity migration contracts.
Tendermint Consensus
protocol by Tendermint
Reference specification of Tendermint's BFT consensus algorithm.
Timewave Vault
protocol by Neutron
specification by Carlos Rodriguez
Quint spec of one way vault for rounding analysis
Universally Composable Security
specification by Denis Firsov (IOG), Pooya Farshim (IOG)
Model-checking UC ideal functionalities, protocols and simulators in Quint
ZKSync Governance
protocol by Matter Labs
specification by Denis Kolegov, Igor Konnov
Gonvernance protocol specification with over 50 invariants
[Your Project Here]
specification by You
Let us know about your project using Quint!