Quint Blog, specs, bugs, and distributed systems

It Told Me No: How Quint Helped Us Fix a Long-Standing Race Condition

The OpenHands team used Quint to debug a stubborn race condition. It told them their first fix wasn't good enough before they shipped it.

July 7, 2026

The Next Bottleneck Is Judgment: Why We're Building Quint

AI can write the code. The bottleneck is now understanding what that code actually does.

June 29, 2026

Catching a DeFi Exploit with Quint: Modeling the Balancer Upscale Bug

How a DeFi exploit hid from every standard correctness check

June 24, 2026

What Specifying MonadBFT Taught Us About Quint

We used Quint to analyze the MonadBFT consensus protocol, formally specifying definitions and pseudo code, validating lemmas and theorems through simulation, and reproducing scenario diagrams as executable runs.

May 7, 2026

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.

April 16, 2026

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

April 9, 2026

Modeling the Faerie-Gold Vulnerability

We wrote a Quint spec for the Faerie-Gold attack in the Zerocash protocol, plus a ZCash-like fix.

March 20, 2026

Towards a Solution for Cognitive Debt

We used to build trust and understanding while coding. With LLMs, we need a new process.

March 9, 2026

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

February 13, 2026

A new LLM-friendly library for Model-Based Testing

We launched Quint Connect, a library for Model-Based Testing in Rust

December 23, 2025

Reliable Software in the LLM Era

How executable specs can be our hope for the future of software

November 17, 2025

Message Soup: the Secret Sauce for Consensus Specifications

The message soup technique enables more powerful specifications. Featuring MonadBFT.

August 11, 2025

How to Write Inductive Invariants

Learn about inductive invariants by defining them interactively with new Quint tools. This post walks through Quint's new --inductive-invariant command, using a Folklore Reliable Broadcast example to show how iterating on counter-examples helps you sharpen your understanding of distributed systems while proving the absence of design bugs.

July 31, 2025

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.

April 1, 2025

Quint Deserves Rust

Why we're rewriting Quint's simulator in Rust for improved performance and more comprehensive testing.

February 18, 2025

Holiday protocols: Secret Santa with Quint 🎅

A fun exploration of drawing strategies for Secret Santa and their properties using Quint. Walk through specifying the game, comparing the redraw vs. reset strategies, and discover why redrawing isn't safe enough to keep Santas secret.

December 23, 2023