Gabriela Moreira
@bugarela.com
CEO at @quint-lang.org. 27 years old, Joinville - Brazil.
Check out my new article "Post Imperative Coding: Executable Specs". #offprint gm0stache.offprint.app/a/3ms4afytfn... #quint #programming
Post Imperative Coding: Executable Specs
How software engineering moves towards specification and validation.
gm0stache.offprint.app
When Charles Hoskinson and his 🐙 call Lean + Quint + Rust "the stack of stacks of stacks," we'll take it. Nothing makes us happier than seeing Quint pushed in ambitious new directions.
Curious about Quint but not sure where to start? This thread covers the open source tooling, and a quick word on what's next 🧵
Maybe we gotta spend some company money and get an octopus to each member of the team 🤔
Quint@quint-lang.org · last wk.When Charles Hoskinson and his 🐙 call Lean + Quint + Rust "the stack of stacks of stacks," we'll take it. Nothing makes us happier than seeing Quint pushed in ambitious new directions.
If AI writes the code, what's left for engineers? @bugarela.com's answer on the @infoq.com podcast: the work that always required the most thought. Defining correct behavior, reasoning about every ordering of events, catching the edge cases. AI won't take the fun part away.
Win of the day: Quint made it into a meme! Thank you dear /u/ThirdWaveCat, this made my day and I got a good laugh out of it 💜
I was a guest on another podcast talking about formal methods 💜
InfoQ@infoq.com · 3w agoQuint specification language is making #FormalMethods more accessible. Learn how AI is lowering the barrier to formal specification and model-based testing - and why defining correct system behavior remains essential human work. 🎧 Listen now: bit.ly/4fbSXjc #AIEngineering #Testing #Culture #Agile
Hey folks I'm looking for some work! Contracting jobs related to ATProto would be a great fit if anybody needs any help along those lines. I'm very good at Rust, I use a lot of TypeScript, and I'm in deep on the Atmosphere. I'm also used to just figuring out whatever I need to. 😁
I really like @slack.com's new feature of link pretty-printing where they strip https:// from pasted links. Such a small thing that actually made me smile a few times this week. Kudos to who had the idea!
New Quint blog! It was very cool when Ray Myers and Ai Vong came to us saying they used Quint to reason about an annoying race condition in Kubernetes. (+) quint.sh/posts/raceco...
It Told Me No: How Quint Helped Us Fix a Long-Standing Race Condition
Quint - Executable specs for reliable systems
quint.sh
"Who knows what's right and wrong is the person building the application. There's so much judgment involved in that." @bugarela.com on what AI still can't decide for you, from her chat on the DevNTell podcast.
"Pokemon" is short for "pocket monsters". "Digimon" is short for "digital monsters". Therefore, "salmon" is short for "saltwater monsters". (You might object: salmon spend a big part of their life in freshwater. But pokemon spend a big part of their life outside pockets too!)
We spent some time polishing and testing those agent-loved markdown files for y'all and we have new skills to share ✨
Quint@quint-lang.org · last mo.Big update to our LLM support. Quint now has easy-to-install agent skills with our main techniques for writing specs and modeling systems. If you've been meaning to write your first formal specification, today's a good day to start.
New post on what that means for engineering organizations and why we're building Quint: bit.ly/3RcE3kV
DevNTell - Quint Co: The Executable Spec Language Made For The AI Era #QuintLang www.youtube.com/watch?v=_8xV...
DevNTell - Quint Co: The Executable Spec Language Made For The AI Era
YouTube video by Developer DAO
youtube.com
Great Article by Adam Chlipala on Why Software Requirements Get Easier in an AI Economy. Formal verification is only helpful if you know what to verify. The spec you check needs to match your intents about what is possible and what shouldn't happen.
We modeled the pool in Quint with the bug present and asked: do naturally-stated correctness invariants find it? Three obvious candidates all missed it for the same reason, they checked outputs, not what the pool stores. Check out the Quint model here: bit.ly/4eLLdod
GitHub - informalsystems/quint-balancer-v2-rounding-bug: Minimal Quint model of Balancer V2 to reproduce the rounding bug
Minimal Quint model of Balancer V2 to reproduce the rounding bug - informalsystems/quint-balancer-v2-rounding-bug
github.com
GitHub Linguist shipped with native Quint support! If your Quint repo has a # mode Bluespec annotation, you can remove it. .qnt files now get proper syntax highlighting and language detection. Our Bluespec era is over. 👋
"There is no magical checkmark for software correctness." At Bug Bash 2026, @bugarela made the case for chasing confidence instead, and showed why the AI era raises the stakes. Here's a breakdown 🧵
This is one of the first dreams I had about Quint: one day, we'll be an official language in GitHub. It warms my heart so much to see this happening, and I feel very good about the new dreams I'm allowing myself to have.
Quint@quint-lang.org · 2mo agoQuint just got merged into GitHub Linguist. Starting with the next release, GitHub detects Quint as a language: syntax highlighting on .qnt files and Quint in the language stats bar. One requirement to qualify: hundreds of repos outside the maintaining org. We're in!
One of the most valuable things about Quint is not just that it finds bugs, it exposes behaviors engineers often don't think to test. The @tur.so team used Quint to model SQLite's C API contracts, automatically generate traces, and replay them against the real implementation.
My talk at BugBash is out!! bit.ly/4ntN4BG I had a blast at this event and I'm really happy with how the talk was received. Hope the recording can reach even more people and shed a light on the topic of confidence and correctness for software 💜 Thanks @antithesis.com for taking care of recording!
Behaviors as the backbone of software correctness | Gabriela Moreira | Bug Bash 2026
Gabriela Moreira introduces Quint (https://quint.sh/), a language built on top of TLA+ to make formal specifications more accessible. Quint was designed at the blockchain company Informal Systems (https://informal.systems/) to solve the syntax and usability problems of TLA+. Her talk focuses on the process of defining correct behavior in software, and then keeping that definition in view throughout the development process, demonstrating how specifications can stay alive throughout development through conformance testing, model-based testing, and trace validation. She introduces techniques for building confidence in specifications including modeling failures explicitly, using witnesses for vacuity checks, and creating reproducible examples that serve as trusted documentation. She also demonstrates how AI can help generate test harnesses and specifications using Quint, making formal methods more practical and accessible to development teams.
bit.ly
Whenever I'm preparing exercises to demonstrate Quint in some way, I struggle to write a model that has bad behavior that needs to be fixed for the exercise. It's something about "making bad states irrepresentable" and how much the data structures we use at the model impact the possible behaviors.
The more serious my work day has been, the more silly I feel the need to be outside work calls. I can't imagine not working remote lol, I'm the kind of person that needs to lay on the ground to think sometimes (often).
The post lays out the general techniques (message soup, sub-protocol abstraction, unfolding recursion into lists) that make distributed protocols at this complexity tractable. bit.ly/4tYIvlF
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.
quint.sh
I've been thinking so much about testing since this conference! If you think Quint can help in your test suite, I'd love to hear about your needs, even if you don't really get what Quint is or do. And looking forward for the videos to be out so you can watch all of the amazing talks that I watched!
Quint@quint-lang.org · 3mo agoThree ways to drive testing from a Quint spec, depending on how much control your runtime gives you: → Model-Based Testing: replay traces from the model → Hybrid: model proposes the next action based on results from runtime → Trace Validation: capture from production, check it against the model
