This directory contains examples of protocol specifications written in Quint.

Note that some examples were written long time ago. All of our examples pass the parser and the type checker, but some of them are not runnable and testable yet. To set your expectations right, check the dashboard below first.

• solidity. The most recent examples of Solidity smart contracts modeled in Quint. This is probably the easiest entry point, as we have been collecting relatively simple contracts so far.

• cosmos. The examples from the Cosmos ecosystem, which we are most excited about. They may be a bit harder to understand though, as we have not polished them yet.

• cosmwasm. Example specifications of CosmWasm smart contracts, another good start for beginners. You may also be interested in our solidity examples.

• classic. These are examples of sequential and distributed algorithms, which stem from the TLA+ examples. These are probably the oldest examples in the repository, so they may use outdated features.

• puzzles. These are logical puzzles. Some people find them nice for learning new languages. If you are one of these people, check the puzzles.

• spells. These are nice small definitions that make specification writing easier. We collect them here. One day some of them will become the standard library. If you think you have invented a nice spell that would help others, contribute your spell.

• language-features. These are examples that demonstrate some language features in isolation. They are mostly used for testing the tool.

This dashboard shows, how far we have checked the examples in the Quint-Apalache pipeline. The reported status reflects running the noted subcommand on the listed without any additional command line arguments.