Alpenglow
Anza Research
Executable specs for reliable systems
Feel more confident about your code (human written or AI-generated)
Executable
Abstract
Programming Languages
define how things happen, in detail
Modern
bank.qnt
/// A state variable to store the balance of each account
var balances: str -> int
pure val ADDRESSES = Set("alice", "bob", "charlie")
action withdraw(account, amount) = {
// Decrement balance of account by amount
balances' = balances.setBy(account, curr => curr - amount)
}
// ...
/// Invariant: Account balances should never be negative
val no_negatives = ADDRESSES.forall(addr =>
balances.get(addr) >= 0
)$ quint run bank.qnt --invariant=no_negativesAn example execution:
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
[State 1] { balances: Map("alice" -> -63, "bob" -> 0, "charlie" -> 0) }
[violation] Found an issue (44ms).
Use --seed=0x4e85b3a53f7ef to reproduce.
Use --verbosity=3 to show executions.
error: Invariant violatedCan you spot the bug? Quint can
Quint is ready to use
The following projects already have Quint specifications
and your project could too
ChonkyBFT
Matter Labs
CometBFT Gossip (Flood)
CometBFT (Informal)
CometBFT Mempool
CometBFT (Informal)
HotShot Epoch‑change
Espresso
Interchain Security
Cosmos Hub (Informal)
Jellyfish Merkle Tree
Left Curve
Malachite
Informal (acquired by Circle)
Minimmit
commonware
MonadBFT
Category Labs
Mysticeti-C
Mysten Labs
Namada
Heliax
Neutron DeX
Neutron
Neutron Drop
Neutron
Neutron Liquidity Pool Migration
Neutron
Tendermint Consensus
Tendermint
Timewave Vault
Neutron
Universally Composable Security
ZKSync Governance
Matter Labs
[Your Project Here]
Tell us about it!