Blog Posts
Introducing Quint: A New Company for a New Era of Software
Quint is becoming its own company, spinning out of Informal Systems to make trust a first-class property of how systems are designed and built.
Two Bugs in the SAFE Predicate: Finding and Formally Verifying Liveness Failures in Byzantine Lattice Agreement
We have modeled the Byzantine Generalized Lattice Agreement algorithm in Quint and found two bugs in the SAFE predicate
Modeling the Faerie-Gold Vulnerability
We wrote a Quint spec for the Faerie-Gold attack in the Zerocash protocol, plus a ZCash-like fix.
Towards a Solution for Cognitive Debt
We used to build trust and understanding while coding. With LLMs, we need a new process.
Model-Based Testing EVM networks with Quint and AI
We used Quint Connect and AI to increase test coverage and find a bug in Emerald
A new LLM-friendly library for Model-Based Testing
We launched Quint Connect, a library for Model-Based Testing in Rust
Reliable Software in the LLM Era
How executable specs can be our hope for the future of software
Message Soup: the Secret Sauce for Consensus Specifications
The message soup technique enables more powerful specifications. Featuring MonadBFT.
How to Write Inductive Invariants
Learn about inductive invariants by defining them interactively with new Quint tools.
Quint Launch Event Follow-Up Q&A and Recap
Recap of our Quint launch event with community Q&A covering formal methods and model checking.
Quint Deserves Rust
Why we're rewriting Quint's simulator in Rust for improved performance and more comprehensive testing.
Holiday protocols: Secret Santa with Quint 🎅
A fun exploration of drawing strategies for Secret Santa and their properties.
Case Studies
Understanding Solana's Alpenglow with Quint
Use the Alpenglow spec to learn about this consensus algorithm in an interactive way.
Espresso HotShot Epoch Changes in Quint
How we used Quint to formalize Espresso's epoch change protocol with executable specifications.
Understanding Mysticeti Consensus with Quint
How Quint transforms complex DAG consensus algorithms into interactive, testable models.
Case Study: Formalizing Grug's Jellyfish Merkle Tree with Quint
Case study on using Quint to formally specify and verify Left Curve's Jellyfish Merkle Tree implementation.
Model-Based Testing Neutron's Liquidity Pool Migration with Quint
Using Quint for model-based testing to discover critical bugs in Neutron's $23M liquidity pool migration.
Talks & Podcasts
Thinking Hard is not Enough
Cosmoverse • Ivan Gavran
Func Prog Podcast Episode
Func Prog Podcast • Gabriela Moreira and Christoffer Ekeroth
![Thumbnail for Introdução à Linguagem Quint [Portuguese]](https://img.youtube.com/vi/IL0ayQDTuIk/hqdefault.jpg)
Introdução à Linguagem Quint [Portuguese]
Esquenta SE4FP • Gabriela Moreira
Live Coding with Quint
BlueYard Capital • Gabriela Moreira
Quint Launch Party
Quint's Launch Online Event • Gabriela Moreira
Quint: A modern and executable specification language
MACROCOSM • Gabriela Moreira and Diego Torres
Modelling and analysis of Starknet decentralization protocols in Quint
StarknetCC • Josef Widder
CosmWasm Contract Security
AwesomWasm Hackathon • Ivan Gavran
Quint - Protocol Specifications Made Executable
ConsensusDays • Zarko Milosevic