Introducing Quint: A New Company for a New Era of Software

Today, we’re excited to share that Quint is becoming its own company, spinning out of Informal Systems.

At Informal, we spent years building large-scale, mission-critical infrastructure for blockchains and distributed systems. In that work, one thing became increasingly clear: the way we build software today is fundamentally insufficient for the systems we are now responsible for.

As systems grow more complex and carry more value, intuition and testing alone are not enough. We need stronger guarantees about how software behaves. This led us to formal methods: mathematical techniques for specifying and verifying system behavior before it is implemented.

Quint is our answer to the problem of trust in software.

From Informal to Quint

Quint was born inside Informal Systems over four years ago. From its early days, Gabriela Moreira picked up the idea, carrying it from initial exploration to a practical tool used by teams today, making it her mission to bring Quint to the world. What started as a deeply technical exploration became something far more important: a practical tool used to design, test, and reason about complex systems before they were ever implemented. Quint evolved not as an academic exercise, but as a tool forged in production environments.

We used Quint extensively inside Informal on real protocols, real systems, and real issues. It helped us catch bugs that would have been catastrophic in production. It helped us explore edge cases that would have been nearly impossible to reason about in code alone.

It also enabled us to build secure software we could truly trust. One example is Malachite, which was built using Quint and acquired by Circle in 2025. With Quint, we were able to move quickly, developing a working consensus engine in a matter of months without being surprised by edge cases during implementation. That confidence translated directly into our ability to bring a compelling, credible system to market.

Why Now?

In the age of AI and LLMs, AI has fundamentally changed how software is built. Code is no longer scarce, it’s abundant.

But this creates a new problem: If code is easy to generate, how do we know it’s correct?

In the age of AI-generated software, verification is no longer optional, it is becoming the central challenge.

We used to build confidence through layers of writing code → writing tests → documenting behavior → conducting reviews.

Now, we prompt and review.

The mechanisms that used to generate confidence are gone. AI makes us dramatically faster at producing code, but it also makes it much harder to know if the code is correct.

This results in bugs surfacing later, systems becoming harder to trust, and high-stakes domains are slow to adopt AI development.

At the same time, formal methods, which were once dismissed as too heavy, too slow, or too academic for mainstream engineering, are becoming newly accessible. AI is lowering the barrier to entry by helping generate specifications that can be checked with deterministic tools. This creates a unique opportunity, as the same force that made code abundant can now help us restore confidence in it.

The challenge is no longer using formal methods, but rather how to integrate them into everyday engineering so that AI-driven spec generation, code generation and deterministic verification tools build a feedback loop that combines the strengths of the involved methods. AI can learn from the output of verification tools and autonomously improve the software artifacts which are fed back into verification tools until the generated software reaches the required level of quality. This brings a new level of automation into software engineering.

What Makes Quint Different?

Recently, specification-driven development has been proposed as a solution to this growing gap between rapid code generation and our ability to check that code matches our intent, defined by a specification. While the idea resonated with us, it relied on the wrong artifact: English and markdown have too much room for ambiguity and leave too many gaps for AI agents to fill.

What if the specification wasn’t something you just read, but something precise you could interact with? Something where validation happens during design, not after code review, and where a single artifact carries through from design to testing to production. What if the spec itself were executable and checkable?

This is what Quint enables.

Quint turns the specification into a living system, something you can explore, simulate, and verify, even before a single line of production code exists. An executable specification closes the gap between intent, code, tests, and runtime behavior.

Quint is not just another programming language. It operates at a different layer of the stack. It is a language for executable specifications, a way to precisely describe how a system should behave, and then run that description.

With Quint, teams can model both happy paths and edge cases in a reproducible way, explore system behavior interactively, and continuously check requirements instead of deferring validation until after implementation. It allows you to verify correctness properties before code exists, while also generating inputs and assertions that feed directly into testing.

Instead of stitching together intent, tests, and monitoring as separate artifacts, Quint unifies them into a single, coherent system.

A Natural Next Step

Spinning out Quint is not a departure from Informal, it’s a continuation of the same mission.

From the beginning, Informal was built on the belief that software, specially systems that hold value, must be trustworthy. That belief led us to formal methods, to protocol design, and ultimately to Quint.

Now, Quint needs its own focus to reach its full potential.

Gabriela Moreira, having worked on Quint since day one, is stepping in as CEO. She is joined by a core team from Informal, including Zarko Milosevic as CTO, Josef Widder as Chief Scientist and Arianne Flemming as COO, alongside a group of engineers and researchers who have used Quint and formal methods in production and understand its value. Together, we are doubling down on Quint with full focus and momentum. After years of incubation, the conditions are finally right: the technology is proven, the need is urgent, and the ecosystem is ready.

Looking Ahead

We believe Quint will become a foundational layer in the modern software stack.

We envision a future where every repository begins with a Quint spec, where intent is explicit, executable, and shared, and where correctness is not something you test later, but something you build in from the start.

As the pace of software development accelerates and the cost of failure continues to rise, trust can no longer be an afterthought. Quint exists to make trust a first-class property of how systems are designed and built.

This is not just a new tool, it’s a shift in how we create software. And we’re just getting started.