Reliable Software in the LLM Era

Reliable Software in the LLM Era

November 17, 2025 • Written by: Gabriela Moreira

Quint was born from the concern of making software more reliable. This has been Informal Systems’ mission from its conception. We want a world where people can trust the software they use.

LLMs have transformed how we write code, but they’ve also created new frustrations. We’ve all been there: staring at a huge AI-generated diff with no clue if it’s actually right. AI fooling us with code that seemed to work but was subtly wrong. Tests that all passed but didn’t actually test anything meaningful. The whole point of LLMs is producing text that looks correct - and that’s exactly what makes validation so hard.

AI is overconfident and needs reality checks.

But here’s the hopeful part: LLMs also enable us to take care of reliability with a much smaller time investment. And no, this is not simply generating specs. It’s not about “putting AI into Quint”. It’s about how Quint fits in the new world of software development, with the same goal it was born with.

Let me tell you how we used Quint to guardrail LLMs and get them to make a significant core change on a complex codebase that we feel confident about.

How Quint fits into this story

The fundamental challenge with LLMs is validation. LLMs excel at code generation, but we humans struggle to validate correctness through code review alone. We typically use a combination of natural language documentation and code, and both are surprisingly hard to validate.

Quint solves this by sitting between English and code as an ideal validation point. It’s more abstract than code, which makes it easier to reason about, yet it’s executable unlike English, which makes it mechanically verifiable. Quint’s tooling - the simulator, model checker, and REPL - lets you build confidence through exploration and property checking.

... continue reading