Understanding Mysticeti Consensus with Quint

Important Context

For this post, it’s important to establish who I am. I’m not a consensus expert - far from it. I work on Quint, a modern specification language, which involves compilers and formal methods. At Informal Systems, we have brilliant consensus experts, but I’m not one of them. My background doesn’t include distributed systems or DAG-based blockchains, so jumping into the Mysticeti  consensus algorithm was a big leap.

At Informal, our consensus gurus are already rocking with Quint (check out Malachite !), so we decided to see what would happen if a “Quint expert tried consensus.” And yes, I started with a complex one.

It worked. And now I feel an (even bigger) urge to teach everyone about Quint so they can also be empowered to learn in this new awesome way.

Starting with the Algorithm

The Mysticeti consensus algorithm is a function that operates on a Directed Acyclic Graph (DAG) that is constructed by broadcasting blocks and information about previously seen blocks. The outcome is a sequence in which blocks should be committed to the blockchain. The algorithm doesn’t need to exchange any further messages at this stage - as for all DAG-based algorithms, the decision is made by only processing the DAG.

In the paper, this function is defined with pseudocode accompanied by some brief descriptions. The hardest part about this project was to understand the paper’s definitions well enough to describe them in Quint (which is not actually understanding the algorithm and how it works). Some of the pseudocode was incomplete, and I found myself juggling terminology from:

• The paper 
• A youtube video 
• The code (from a prototype) 

Since I’m not from the consensus field, there were definitely gaps between the assumed prior knowledge in these resources and what I actually knew.

My first attempt at translating the algorithm into Quint was incorrect. But through iterative refinement - using visualization and testing - I eventually arrived at a version that aligns with the paper’s description. This process showed me how Quint isn’t just a tool for experts; it’s a tool for learning.

Visualization: Seeing the DAG

A DAG is a graph, and graphs need to be visualized. Even with Quint’s clear traces, I couldn’t fully grasp what was happening without drawing it out. So, instead of banging my head against Quint traces, I:

1. Asked Quint to export traces to JSON.
2. Used an existing Rust trace parser (itf-rs ).
3. Got my AI buddies to help me build a custom visualizer.

As I iterated, I realized I was missing some critical information, like certificate patterns and certified links. So, I enhanced my model to track these edges and visualize them alongside the DAG. This turned out to be a game-changer, especially during the testing phase.

Testing: Validating Against the Paper

I was still lacking some ground. Ok, I wrote my definitions, not sure if I understood things correctly - how can I know if my specification is the same as what the paper describes?

Luckily for me, Appendix A of the paper included a detailed description of a concrete execution. This is exactly what I like using Quint for, as understanding specific executions is a super important step to understand algorithms. So I wrote a Quint run that:

1. Took the DAG from the paper’s example as input.
2. Executed my function step-by-step.
3. Compared the results at each step with the paper’s description.

As I was collecting additional data, I could also compare how the result was obtained - either through direct decision or indirect decision, and which block was used as the anchor in indirect decisions.

This test didn’t pass initially, and debugging was tricky. But with the help of my visualizer, I could compare my DAG with the paper’s diagrams and identify where I’d gone wrong. Iterating with the visualizer was not only effective but also incredibly satisfying. It transformed a frustrating process into an engaging one, and this part of the process is what taught me the most. Quint’s ability to generate traces for visualization was essential for this iterative learning process – a consistent benefit I’ve found when using Quint to understand distributed algorithms (see this  for another example).

Checking a Property in the Test

While I could validate my model against the paper’s example, I wanted to go further. The most important property of the Mysticeti protocol is the total order property: all correct validators must commit a consistent sequence of proposer blocks. In other words, the committed sequence of one validator should be a prefix of another’s.

To test this, I:

1. Added two new blocks to the example DAG non-deterministically.
2. Calculated the commit order for three scenarios:
   • DAG with only the first block.
   • DAG with only the second block.
   • DAG with both blocks.
3. Verified that the results of the first two scenarios were prefixes of the third.

This was the first non-determinism introduced to this model, and it was in the form of a property-based test. I used quint test to fuzz this and it couldn’t find any violation - it felt like my model was on the right track.

A State Machine for DAG Evolution

Testing on a single example DAG wasn’t enough. I wanted to check the total order property on arbitrary DAGs, but I didn’t yet understand the rules for creating a valid DAG. This led me to collaborate with my colleague Martin Hutle, a consensus expert, during Informal’s team retreat in Paris.

Together, we defined a state machine called DAG evolution, which describes how a DAG can grow over time. The model includes:

• Some defined number of validators, each with their own local version of the DAG.
• Messages between validators that update the DAG.
• Byzantine nodes that can send malicious messages (the trickiest part to define).

This state machine is reusable, and while we haven’t yet applied it to other DAG-based consensus algorithms, it’s a promising foundation for future work.

Putting It All Together

With the state machine in place, I could now check the total order property across all states. For each state, I evaluated the consensus function for each correct validator’s local DAG and compared the resulting commit orders, ensuring that all commit orders were prefixes of one another.

I ran a few thousand simulations with both the existing Quint simulator in Typescript and the new Rust simulator (see Quint Deserves Rust) - none of them could find violations.

Quint: A Tool for Understanding

The biggest takeaway from this journey is that Quint is more than a formal specification tool—it’s a tool for understanding. Its ability to formalize concepts, facilitate interactive exploration, and enhance precision makes it invaluable for tackling complex systems. Whether you’re a researcher, engineer, or just someone curious about how things work, Quint can help you uncover the mysteries beneath the surface.

Beyond Papers: The Power of Interactive Artifacts

One of Quint’s standout features is its interactive nature. Unlike traditional research papers, which often leave room for ambiguity, Quint provides a hands-on, explorable artifact. This is especially valuable for complex protocols, where static descriptions can fall short.

“Writing is nature’s way of letting you know how sloppy your thinking is.” —Dick Guindon

“If you’re thinking without writing, you only think you’re thinking. […] Everyone thinks they think. If you don’t write down your thoughts, you are fooling yourself.” — Leslie Lamport

Lamport created TLA+ to help people define their algorithms precisely, and we created Quint to make this more accessible and help people get the most value out of these precise descriptions. Writing in Quint forced me to think about Mysticeti much more precisely, and anyone who uses this Quint specification to learn about Mysticeti will have a significant head start.

All this work is open source and available at Informal’s GitHub , including:

• Specification of Mysticeti consensus
• Specification of a DAG evolution state machine
• Visualization tool

Embrace Quint for Your Next Challenge

So, if you find yourself grappling with a complex system like the Mysticeti consensus algorithm, and you’re seeking a deeper understanding - why not give Quint a shot?

Quint’s blend of interactive exploration and unwavering precision could be your key to unlocking clarity and insights that other methods simply can’t offer. It takes learning, but it is worth it.

Check out Quint at quint.sh ! And if you are looking for a precise specification of your own algorithm or protocol, reach us at audits@informal.systems, or find us on our website .