Quint Deserves Rust

We’re excited to announce that we’ve embarked on a new project: developing a Quint simulator in Rust! This decision comes in response to community feedback and our ongoing commitment to improving Quint’s performance and scalability. We are hitting bottlenecks from having the simulator in Typescript and are ready to move on to the next level with this core performance-sensitive component of Quint.

Why Rust?

Our current Quint simulator, written in Typescript, has served us well. Although performance has never been a primary concern (over user experience and extensibility), we can now see how much the simulator speed impacts our day-to-day job and the main Quint goal of giving us confidence. The more we use the Quint simulator, the more apparent it becomes that faster simulation speeds would allow us to run more simulations in the same amount of time. More simulations means more confidence because we get to explore a larger number of different traces and potential edge cases.

We have plenty of in-house expertise in Rust and have built amazing Rust products (see Hermes  and Malachite ). And - in case you haven’t heard - Rust is the best language out there for performance-sensitive apps. This is the main motivation for choosing Rust. As language designers ourselves, we also recognize and heavily appreciate the expressiveness of the language and enthusiastic community of Rust, which align perfectly with our goals for Quint.

Good News for Us

Before starting this project, we conducted a preliminary research to answer the question: what is the most performant way to write an interpreter in Rust? We ran benchmarks for five different approaches  and the winner was an approach using a form of partial evaluation of the program into native Rust closures. And that was really really cool, since the current implementation in Typescript uses the same approach! We really were hitting a bottleneck in Typescript and had already optimized the code a lot. This means we can re-implement the simulator in Rust using the same approach, making this rewrite much more efficient and predictable.

We also found a Cloudflare article, “Building fast interpreters in Rust ,” which explored various options and ultimately chose an approach with dynamic dispatch and closures. This approach aligned with ours and reinforced our confidence in our chosen direction.

Objectives

We won’t rewrite all of Quint in Rust, at least not now. Many parts of Quint are not sensitive to performance, especially since Quint projects will never have thousands of files - it is a specification language where we tackle parts of a system at a time. It doesn’t really matter if the parser or the typechecker are sub-optimal: the bottleneck will always be the simulator, which we want to use to run as many simulations as possible.

Therefore, we’ll only rewrite the simulator. Quint tooling already interacts with Apalache, which is written in Scala, by exchanging JSON through an RPC connection. The Rust simulator can use that very same JSON format as input and output. We don’t want to add any complexity to Quint users - it will be all set up automatically like it is done for the Apalache integration. They will just notice it is faster 😎.

We also want to move eagerly for benchmarks. Even though we strongly believe that the performance benefits will be worth our time spent in this rewrite, we want to have that information as soon as possible. We will prioritize work paths that will result in us knowing whether it is worth continuing.

Anticipated Benefits

These are the reasons why we are so excited:

Improved Performance

Rust’s amazing memory management lets us control how memory gets copied and allocated, which we couldn’t in Typescript. For example, our current implementation in Typescript defines interfaces to act as pointers as a workaround for that lack of control where it is absolutely necessary (to avoid running out of memory when simulating millions of samples). We won’t have that problem in Rust, where we can choose when to pass around and mutate data by reference or by value.

On top of eliminating this bottleneck of memory management imposed by Typescript, Rust itself is already faster - we expect that a direct rewrite will already make the performance better, while unlocking more optimizations we can do in the future.

More Maintainable Code

I probably don’t need to dive into how amazingly expressive Rust is in this post, so I’ll just mention pattern matching, traits and the question mark operator. We are already leveraging those so much in the first lines of code, resulting in a code that is much easier to read and maintain. Future us (Quint maintainers) will be grateful.

Expanded Community

One of our initial motivations to write Quint in Typescript was to maximize the number of people who could collaborate on the project or extend it. We wanted people to feel empowered to dive into the code, and Typescript was (and still is) a very popular language, and a language that people wouldn’t be scared by.

We didn’t take communities enough into consideration. So far, we haven’t found a lot of natural overlap between the Typescript community and the (potential) community of Quint (protocol designers, compiler engineers, formal methods learners/users, security auditors, …). Rust’s community, however, has a bigger intersection. By embracing Rust, we hope to engage with a broader community of developers and researchers interested in formal specification and verification.

Project Milestones

We have started this work in 2025 and things are moving quickly. Here are the milestones we have planned:

• [DONE] Deserialization: Parse the Quint IR (Intermediate Representation) JSON in Rust. Done! Thank you serde.
• [DONE] Evaluation for built-ins: Write translation into closures for all the stateless built-in operators. Benchmark. With lots of help from AI code assistants for the boring parts of a direct rewrite (including a big suite of unit tests we imported from the Typescript implementation), this was done in a couple of weeks! The hardest part was to figure out the lifetimes of some closures, especially for the interpretation of Quint lambda expressions, which re-use the same memory space for different evaluations. Benchmarks at this point are not very reliable, but we’ve seen some great numbers in preliminary experiments 👀.
• Statefulness: Store state and modify it with steps and assignments. Benchmark.
• Nondeterminism: Implement the oneOf operator for different values (which includes a bunch of optimizations - we won’t enumerate big complicated sets just to pick a single value out of it). Benchmark.
• Simulation: “For N in number of samples, for S in number of steps, run init then step (S times), checking invariants and witnesses at every state”. Benchmark a lot. At this point, we have all the benchmarks we need, and everything from here is just polishing. We plan on starting to use this internally already at this point, wiring things together manually while the integrations are not complete.
• Simulator integration: Call the Rust simulator from the TS CLI.
• Evaluator integration: Evaluate REPL expressions and definitions through the Rust evaluator.
• Support for multiple modules and constants: Handle the manipulation of namespaces and constants required for multiple modules.

Stay Tuned!

This is a very exciting project for us and we will continue to share updates as we progress. We believe that a Rust-based Quint simulator will be a valuable addition to the Quint ecosystem and are eager to see the benefits it will bring. Follow @bugarela  on X for sneak peaks!