Projects
![]()
No projects found
Investors
New
DAO Treasuries
DATs
Lend / Borrow APRs
Chains
Categories
Spaces
Launching Choreo on Quint Q&A
Recorded: Sept. 23, 2025 Duration: 1:03:09Space Recording
Short Summary
Choreo's launch marks a significant advancement in the Quint ecosystem, aiming to simplify the development of distributed systems. With strategic partnerships and a focus on accessibility, this new framework is set to drive growth and innovation in the blockchain space.
Full Transcription
Thank you. Thank you. Hello, can you hear me?
I think it works because I see the animation moving.
Okay, I kind of heard you, Ocean.
I couldn't really hear what you said, but I think it works. Thank you. Good morning or afternoon everyone.
We're just waiting for our speakers here so get comfy and we'll let you know when we're Thank you. . Thank you. All right, I think we have everyone as speakers now, so I'll pass it off to Gabrielle and
Ethan.
Hi, everyone.
Thank you for joining our spaces.
We're excited to talk about Choreo.
Ethan, do you want to test your mic?
Hello, hello.
Hello.
How's it going?
I'm good.
How are you doing?
I'm good.
I'm very good.
Very excited.
First day of spring.
I guess it's fall for you guys, but I'm very happy.
Yeah, nice.
So, now, finally.
So, yeah, jumping into Choreo.
So, just a very brief overview.
Corel is this new framework that we launched for Quint.
One thing that people would say about Quint sometimes
is that it doesn't feel batteries included
because Quint is very general.
So you can specify basically anything you want in Quint.
I specify like some games, some...
I've even thought about like managing my cat's litter box in Quint.
So it's very general. You can think about any state machines in Quint.
But mostly what we are doing is just specifying distributed systems.
Sorry, what is the state machine for your cat's litter box?
So basically, if you have a cat, you kind of have to clean the litter box, at least
with some frequency in order to see if there is like some problems, you know, like if there's
blood in there, then you must get to the vet in like 24 hours.
Otherwise, it can be something very serious.
So in order to do that, then you have to have at least some frequency for checking the litter
box and cleaning it.
So I was thinking if we can have this property, you know, like in Quint and having the state machine of like,
okay, if you clean it at least like once a day, then for sure you'll get to the vet in enough time if something happens,
depending on the time of detection of diseases.
You're not worried about like race conditions with the cat or some kind of deadlock.
There's no distributed protocol. No, no, that's all fine. Okay. Yeah, that's all fine because I
only have one cat, you know, so no problems. I have two litter boxes. And Quint is still useful
even for sequential protocols. Yes, I think so. I've used it for some sequential thinking, I guess.
It's harder or it's rarer for it to be used
for sequential protocols because it's usually less complex.
So you only get used if it is actually complex
and you don't, you cannot think of it in your head.
I guess the litter box is something
that I can think of in my head.
So it's not a super good example, but it's a fun one.
But it still gives you a delightful form of language
to express your program and invariants and actually check them so that, you know, even if it's sequential, if it's hard to keep all the pieces in your head, Quinn's still useful.
Yes, yes. I have a good example for that as well.
So I was teaching formal methods at the university and we wanted to kind of like have seminars and people would choose the subject
they wanted to talk about.
And I wanted to kind of like raft the teams
between the students, you know,
refl I guess is the word, sorry.
So I wanted to do some sort of like random assignment,
but I wanted to follow their preferences.
So I modeled something saying like, there couldn't be, so if I chose,
so the seminars were on formal methods as well.
So if I chose to speak about cock and you,
and my second preferred one is Quint,
and your preferred one is Quint,
but your second favorite is Lean, right?
If I do an assignment where I have Quint
and you have Coq,
that's not good because I would prefer having Coq and you'd prefer having Quint.
If there was such a scenario, then that solution was not good.
I wrote this in Quint and had Appalachian,
the mother checker find me a solution where I could have
an assignment to each student that had the preferred team.
It's not a complex thing,
but it would take me a while to figure this out by hand.
So you were actually looking for a result that you were like, like an implementation
outcome and Quint just like, you know, found it quickly for you.
Do you think it would have been like, that's something that you could imagine someone else
imagine someone else doing a similar thing and writing it in Python. Do you think, you know,
doing a similar thing and writing it in Python.
Quint has a future as a scripting language like this for quickly figuring out real world things?
Yeah. Well, for me, it was because I didn't have to. So one thing, interesting thing about the
formal specifications is that you don't have to tell it exactly how to do something. For example,
you can define a sorted list as a list where
every consecutive element is greater than the one before. That's a sorted list. You don't have to
use quicksort, you know? So that was kind of what I did. I specified what was a correct solution,
and Quint gave me the results without me having to write a matching algorithm or whatever I would
ask for that. Very cool.
Okay, well, this has all been a tangent
from what we're trying to talk about today,
which is distributed protocols.
And Corey, why don't you continue
a little introduction that you started
before I started questioning you about cat litter.
Okay, yeah, so when people were using Quint
to write distributed protocols,
which I guess was pretty much most of our usage,
they would miss things.
Like, how do I do message passing?
Oh, you have to do it like this and that.
So we have to explain to these people how to do it every time,
or they would have to figure it out every time.
So if every single Quint spec that we are writing,
or most Quint specs that we are writing or most Quint specs that we
are writing need message passing, why it's not there? So people ask why is it not berries included?
And we don't want to change Quint. We want Quint to still... Not for this, right? We still want
Quint to be a very general tool that people can use for very different things because it's a general language. We don't want to make it like a DSL, right? But we could make a library or a framework. So
that's what we started doing. And there were some challenges because Quint is not a programming
language. It's not meant to be super extensible in this sense because also we don't want to have huge specs because that's not the goal.
It's like having very abstract scoped specs.
But yeah, so we started in this task
and we have Yassin who is here with us today as well.
He joined Informal as an intern
and he took on this task very seriously
and he ended up writing his master thesis about this.
So it was very interesting project. So that is Corio and how it was born. on this task very seriously and he ended up writing his master thesis about this so
uh it was very interesting project so that that is choreo and how it was born
amazing
so it needs so it ended up that choreo uh i guess it has two main advantages first first it's very
like easy to onboard and start using,
or start writing specs for distributed systems now.
I guess Quint already makes it much easier
than with some other tooling that is available
because we have a much more accessible language,
but Choreo makes it even easier if that's possible
because it adds this construct and this structure for you to start writing.
So you actually can download our template
and start from there.
You're not obligated to use the template,
but the template can help you already have some structure.
So instead of starting with a blank file,
you go there and there's like to do,
put your types here and then put the types there.
And then it takes care of, and then it helps to get started.
And the second advantage is that it will,
you will only, you not only write a distributed system spec,
but you're actually going to write a good one,
probably better than people that get started
with other languages,
because this already embeds some techniques,
a formal specification that people probably wouldn't
get learned so quickly uh without studying a little bit at least okay maybe maybe let's back
up a bit let's let's start with the name why is it called uh why is it called choreo oh that's
names are super hard right so we had some iterations um and i i liked course. So first of all, I was a dancer. I like to dance. So I
have a good excuse. But we were thinking about this, like orchestrating distributed systems
and how hard it is to think about many processes and put them all in one place and the non-determinism.
And then I was mostly talking to ChatGPT and Yassine was also talking to ChatGPT
and Yosef, we are using like,
can you please give us ideas for the names?
And one of the many names that we went to was Choreo
and I immediately liked it.
And I liked the hook,
Choreographing Distributed Systems
because that's what we are doing, right?
So when you're choreographing,
you have like this group of people,
everyone goes in a different direction. They have to go there and form a circle and the other one comes here and forms a line. doing, right? So when you're choreographing, you have like this group of people, everyone
goes in a different direction, they have to go there and form a circle and the other
one comes here and forms a line and you have to take care of all of that. And in the end,
it's something beautiful, but what every single dancer is doing in a choreograph, like you
have to worry about so many things. So I think it makes a lot of sense.
Right. So Quint is already, you know, even before Coreo, Quint was heavily used for specifying distributed systems, arguably one of the best tools on the planet for doing so.
So, you know, one might come to this and say, well, isn't Quint already, wasn't Quint already designed for specifying distributed systems? Why have you gone and had to, you know, create a
framework that you now say is for specifying distributed systems when you already had,
you know, a specification language for doing it? What, maybe you can talk a little bit about what
makes it, even when you're using Quint, what makes it difficult or challenging
and to specify distributed systems and, you know, if Quint is supposed to help you reason about them,
why wasn't Quint enough?
What sort of motivated the introduction of Choreo?
Yeah, good question.
So Quint is based on CLA+, right?
And the creator of CLA+, is Leslie Lampard,
which is a very influential person
in this distributed systems world.
And he created CLA person in this distributed systems world and he
created tla plus because of distributed systems he was writing papers on distributed systems and he
lacked a precise language to define and reason about these systems for those who don't know this
is the guy that coined the term byzantine uh byzantine general problem byzantine fault
tolerance all of us in blockchains are very much directly downstream of this guy. He invented the Paxos algorithm and he invented latex, right? And
TLA because latex wasn't torture enough. He needed to torture people in other ways when
they think about protocols, but it was supposed to be helpful. This TLA plus thing, right?
Sorry, go on.
Yes. Yes. So if you Google Byzantine fault tolerance, go to the paper,
you'll see that Leslie Lamport is the author. Yeah, so he created TLA plus for this,
to be precise when he talks about distributed systems to other people. And we created Quint
based on TLA plus, but TLA plus is very mathematical and it's meant to write papers.
And we don't want to write papers.
We want to write executable specs.
So Queens is a much better language for executable specifications.
Right.
Because TLA plus is not executable.
So it's model checkable and it's simulatable,
but it was not created to be anywhere near a computer.
You know, like,
Lambert didn't think
you could even write a model checker for TLC.
For TLA, sorry.
Later, the TLC was created
but, like, the amount of work
you have to do to even
parse the language
because it was not meant for that.
It is meant for that.
So TLA plus was very
much designed as, you know, a tool in the logicians toolbox to be something for thinking mathematically,
but it was very mathematician oriented. It wasn't really designed to be part of, let's say, the
software development lifestyle to be really accessible to software developers to be part of,
you know, to have tooling that, you know, that allows it to be quickly executable
and integrated into your flows and things like that.
It was really for like, as if you were going to sit down with pen and paper, but, you know,
do it in latex kind of thing.
Yes, yes.
And have a precise language.
Because in the papers, if you, Lampard said like, he was writing the papers in English,
writing the papers in English, right? So he writes like, oh, if this happens, then that should
right?
So he wrote like, oh, if this happens, then that should occur.
occur. And he noticed that even he had ambiguities in his papers. And he said, oh, if I,
who am very smart and a very good writer can be imprecise, imagine the others.
Yeah. And that's, so the main motivation is precision. And then the other stuff came later.
So today they do have initiatives to make TLA plus more accessible.
For example, with plus call, they do have a lot.
They try to give TLA plus for the engineers as well.
So today, definitely that's one of their goals.
They want more engineers to use TLA plus.
But it's an afterthought.
It wasn't designed for that.
And so it's lacking a kind of, you know, let's say,
aesthetic of modern development tools. Yeah, and it's super hard to do these tools as an afterthought. Right. Certainly. They have many difficulties. Right.
Okay. Yeah, please. Yeah. Zampart designed it for precise and precise way of talking about
distributed systems, and then Quint is based on that.
And so when we first wrote the readme for Quint,
we added like for distributed systems,
focus on distributed systems.
Cause I think the very like necessity of right,
sitting down writing as formal spec with the state machine
matches the distributed system setting a lot because the pain
point that we have in distributed systems where it's so hard to think about all the stuff that
can happen, the interleavings and everything, it's so hard. And that's why formal specs are a great
fit and Quint is a great fit. So you know how the relationship between Quint and distributed systems
is, it exists, but it's not like completely direct. It's because distributed systems are difficult
and Quint helps with difficult stuff. Does that make sense?
So it's a general tool for understanding that is really just a more delightful
wrapper around mathematics, essentially. That's really what Quint is under the hood, is just a way to express math in a more, you know, familiar and accessible language.
And of course, that can be used for modeling distributed systems protocols, because those
are just math. And those are the kinds of protocols that will benefit most from, you know,
sitting down and writing some math about them. But Quint is a generalized language.
It's math, and so it can be used for anything. It doesn't have built-in helpers to actually
model specific things about how... You still have to make a lot of decisions when you sit down to
use Quint on how you're going to model the distributed system. How do you model the environment? How do you model the
message passing? How do you model, you know, a Byzantine actor who's, you know, trying to mess
with your protocol? You have to make all these decisions on how you're going to model your
distributed system. And you have to do it each time you sit down to model a distributed system
in Quint, right?
And so that adds just, you know, it makes it harder, I guess, than it needs to be.
Whereas Choreo is making a lot of those decisions for you.
Is that right?
Yes, precisely.
Exactly that.
Yeah.
So for people that are not used to modeling distributed systems or doing it for the first time,
then they have to learn and think a lot if they're using just raw Quint. And for us who are used to it and they're doing
all the time, it's like boilerplate we have to write and then more things that we need to set
up. And Choreo solves those. Right. And so I imagine, you know, we've been, you and our team
and others now have been writing Quintpecs for distributed systems for a number
of years before choreo existed so i imagine there's a number of different ways out in the wild
that folks have gone about you know actually modeling these different components of distributed
systems and there's been some comparison between those some contrast some lessons learned can you speak to any of that
yes um i guess the most uh concrete example or instance of this that i can talk about
is about message passing so if you even go into the lampard's website and watch his lectures which
is how i got into this world right i that's how I learned this stuff. It's by Washington Lambert.
And he teaches you that when you are modeling message passing,
you should just have a set of elements.
So you have a state variable,
which works sort of like as a global variable
that changes over time in your state machine.
So you start with a perhaps empty set of messages.
And then as the processes start
to communicate, you just add new messages to the set. And then receiving a message means just
looking at the set and checking that the message is there. So if there is a message in the set of
all messages ever sent, then that means you can receive that message. You don't take it out of
the set. It's still there. And that's how we modeled message passing in most form of specs.
That's how Lampard taught us to do it.
And that's not the most intuitive way at all.
Maybe the most intuitive way is having like an array with a queue,
or maybe an internal buffer for each of the process
with the messages it has to receive.
And then it starts consuming them and removing them from this list in certain orders but the thing is that the having
a set is very general but having a set I mean does that prevent you from receiving the same message
twice or I guess the message persists in there so you could read it multiple times and that's
how you would model receiving the same message twice?
Yeah. So you, the set doesn't prevent that. So you can receive the same message multiple times, which is basically it's modeling this at least once delivery model, or maybe
since we are choosing from the set, which message you are going to receive in a non-deterministic
way, it can also mean that you never receive some message or receive some message that was sent later
before a message that was sent before.
So there's no ordering guarantees.
So this is like the most general modeling.
It takes care of all the problems
that can happen in real life in the network.
So it's very general and it's very efficient.
Right.
So is that technique built into Choreo then?
Yes, it is. Okay. So if you hadn't come across that, you know, these Lamport videos, or you
hadn't learned or thought about this somewhat unintuitive way of modeling messaging, you might
be trying to do something else that might complicate the specs in ways you didn't expect or,
complicate the specs in ways you
didn't expect or
wouldn't want.
Yeah, exactly.
I guess either you wouldn't know how to do it
at all and you would look it up
on the internet and maybe find out the proper
way or maybe you would try it yourself
and then you would probably end up with
something like the internal buffer arrays
that I mentioned.
And is this set what we call
the message soup
in our blog posts and other places?
Yes, yes.
Okay, great.
So even before we posted, we published Corio,
we're already exploring this stuff.
And we actually went and tried to validate this
because how we ended up writing this blog post, okay?
So we wanted Corio to be super simple to use.
And the simplest thing to use,
or if you're coming from like a pseudocode for a protocol,
is usually like you receive one message
and then you do something about it.
So like upon a proposal, you do something.
Upon a message of certain type, you react like this.
People usually write their pseudocode.
I mean, that's how you'd write the code, right? You'd write a handler for the message, you receive the message. You know, you run like this. People usually write their pseudocode. I mean, that's how you would write, that's how you'd write the code, right?
You'd write a handler for the message,
you receive the message, you know,
you run through your handler, you stick the message,
you update your state based on that, you're accumulating.
Usually you're trying to accumulate votes or signatures
or something until you hit some threshold, right?
And so you do it one message at a time, right?
That's what you're talking about?
Yes, yes, exactly.
Yeah, the code would be a better example, yeah.
So that's how you write code.
If you're doing something simpler than consensus,
if you're consuming from a PubSub channel, you get a message,
you do something about it.
If you have a queue of messages, you just get a job
and do something about it.
So it's natural that someone would think
to write their spec in the same way
as they write those handlers.
Yes.
And so we wanted to put this in Corio as well.
So we want to, like, oh, you don't think about, like, actions, transitions, state machines.
You just write these handlers for single messages, and then you're done.
And I was really pushing for this.
Like, I really wanted this to be super easy.
But this is not super compatible with the message soup technique.
It's still, like, I can still consume messages from the set like this, so it still works.
But it is not the most efficient way of writing it.
I'll explain why in a bit.
But we are trying very hard to have this the easiest way possible.
And we started doing benchmarks and running like estimating the state space
for different approaches,
MessageSoup without MessageSoup,
removing messages or not removing messages.
We tried a bunch of things.
That's also what's in the blog post.
And we ended up like showing with the data
how this MessageSoup technique is actually the best
and how you shouldn't receive,
you shouldn't think about handlers message by message.
So not thinking about receiving one single message and then you receive another one and then you receive another one.
So this is not the most effective way.
And Choreo, so you can write it like this with Choreo.
So you can write it like this with Choreo.
There is an option for that.
But the main option that Choreo offers you,
like the tutorials talk about,
it's not message by message.
It's more like you look at the message soup
and see what's in there.
So if you're thinking about Quorum, for example,
so you want to have, for example, in Tendermint,
you want to have three pre-votes before,
or three in a system with four nodes, right?
You want to have at least three pre-votes
before you proceed, right?
So you need to have quorum.
So what you can do if you're thinking about handlers
receiving a specific message,
and then another one, another one,
what you have is like you receive one pre-vote
and then you do something like increment
your internal counter or your internal registry of the votes you received. Then you
receive another vote and then you increment that again and then you receive another one and then
increment that again. Oh, now I have quorum and then you do something. So this is like a lot of
transitions in the state machine. While if you know that you have this message soup, right? So you
are aware that the message soup is there and exists.
You don't have to receive all of those messages.
You can just go and look at the message soup and say,
oh, there are three pre-votes here in the message soup.
So I can kind of like, you don't actually receive those.
You just know that it's there.
And since the messages are there,
then it means you can do your thing.
You have quality.
Interesting. So really, you know, the key point here is what we're saying is, look,
we want to be able to model the system effectively so that we can understand it.
And the way we implement it, we don't have a choice when we implement the system,
but to write a per message handler. We have to, you know, it's a device,
it's separate from the network. It has to receive the message, process it, you know, update the state, whatever, because it has
to accumulate, you know, something, some counter, you know, pay attention until it reaches the
threshold. But when we're modeling the system, what we actually care about is the state change
on the threshold. And if we were to, if we we model the system one message at a time, then we're treating each message as if it's its own state transition, right?
Which isn't actually true from the perspective of the protocol.
It's true from the perspective of the code.
We're going to have some state variable and we're going to add the effect of each message to that state variable, but nothing is going to happen even in the code at a protocol
level until we cross some threshold. So when we're modeling, it actually will be much more efficient
and it provides a better abstraction if we don't think about things one message at a time. And if
we don't, you know, have each message imply a state transition,
but rather we just allow the messages
to accumulate in the soup, and the only state transitions
we want to have in the model are the actual state
transitions in the protocol, which
are when we reach thresholds or meaningful events happen
that don't just happen one message at a time.
Is that the idea?
Yes, exactly.
So if you think of a state machine, right?
So in state machine, you have circles and arrows.
If you're going with a message soup and you start with a circle where you haven't reached threshold and you receive a message
and you are in a circle where you have the threshold or have quorum
and then you go to a circle where you do something based on quorum.
So it's very, you know, like there are three states in there in this, in this part.
While if you are receiving message by message, then you have a bunch of orderings in which
you can receive them.
So I'm thinking, I'm talking here about three messages.
You can receive first A, then B, then C, or you can receive first B and C, then A.
So all of these orderings, and when you're doing formal specifications
you are going to simulate or model check all of these possibilities so the more you have the the
like you're spending a lot of computing on this different orderings and for your protocol it
doesn't matter you receive the pre-votes right so it just explodes the state space and you get this
combinatorial explosion that makes it harder to actually do any reasoning or modeling or finding traces that matter, things like that.
Yes, yes. The finding traces that matter might be the highlight here.
That's what we talk about in the blog post as well. bunch of interesting states that we want to see that we try to find using simulation.
And we see how using this technique, we can find these traces much quicker.
And even in some cases, using the message-by-message approach, we don't find those scenarios. While using this message soup technique, we find them very quickly.
Yeah, that's super interesting and compelling. It sounds like, I mean, this thing
about maybe you want to just talk about traces for a minute and what's useful about traces and why,
you know, why should people care about traces and what do they do for them?
Yeah, I guess there's so much things to think about traces. Traces are my favorite thing, maybe.
Traces are an amazing way of understanding what's happening. I think even when we started Quint,
we underestimated a bit traces. Because we started doing the Quint simulator for
just because people asked for it, but we had a mix of intentions. But when we run the simulator,
and it's super fast, you can run the simulator for one single sample,
which it's like instant.
And then you get one trace of your application
and then you see what happened in this like abstract level.
Cause when you are working with Quint and Corio,
you have a very abstract level of understanding things.
Seeing a trace of Tendermint helps you understand it so well.
It's so good.
And then you can use the traces for
testing, for example, your application. So just to clarify, like when we write a spec,
it's an abstraction, it's kind of lifeless, it's just supposed to state what the protocol does and
how it behaves, but what we actually want isn't just to like reason in the abstract about the protocol we care about you know ultimately a real implementation and being able to debug it
and all of these things and so the traces are actual concrete runs through the the protocol
specified and quit right they're the actual set of states and state transitions that might occur
and of course for any given protocol spec,
there could be a zillion possible traces, right? Like the set of all possible traces is really the set of all possible states and state transitions that the protocol could execute through.
But the, you know, the Quint tooling has been somewhat specialized to provide traces and make it so that users can
actually reason about the protocol using the traces rather than just the abstract spec.
Because if you're stuck at the abstract spec, then you yourself would have to like go and think
through, okay, this happens and then this happens and then this happens. Well, what if this happened
and then would this happen, right? And you're like kind of walking through it yourself, whereas the traces kind of do that automatically.
So the simulator will actually, you know,
it'll randomly run through a bunch of possible states
and state transitions and give them to you as traces.
And then you can inspect them to actually understand
how the protocol logic flows in a real concrete run, right?
Yes.
And one of my favorite use cases for that
is this sort of like witnesses
where you can find interesting scenarios.
So if you're, so a queen spec per se
is very similar to like pseudocode in a way.
So if you're only looking at it, if you're not running it,
so it's very similar to pseudocode
where you have all the things that can happen
in a high level of abstraction.
And if you're like me, maybe you already looked at some pseudocode and we are talking about this like handler sort of perspective, right?
So like, oh, when you receive three proposals with value minus one, then, and you had a timeout and blah, blah, blah, then you do this.
and you had a timeout and blah, blah, blah,
then you do this.
So you look at the pseudocode
and you have this very specific reactions or handlers
and you're like, okay, but why do we need this?
When is this useful?
When is this going to happen?
Like there must be a way
because the people who wrote the paper are very smart
and there must be some scenario that needs this,
that requires these mechanics, this mechanism.
But I don't know when this is necessary.
How can I figure that out?
You can spend maybe hours on paper playing with scenarios
and trying to understand how you get to that.
But we, Quint you can just ask like, hey, Quint,
can you get me a scenario where this thing right here
is executed and then Quint will give you,
and then you can understand like, oh, okay, that's how. So you time out here and then quaint will give you and then you can understand like oh
okay that's how so you time out here and then two states later you receive this type of message oh
okay now right so there might be what you're saying is there might be some part of the spec
that you know that describes some part of the protocol that is maybe covering
like the unhappy path right where some complex sequence of things happens and you have to
account for it.
And it's not clear just by looking at the spec,
like what would lead you to that state
where like this part of the protocol kicks in, right?
But with Quint, you can say,
hey, give me a trace
where this part of the protocol kicks in.
And then Quint will just spit out the trace
and suddenly you have a, you know,
exact sequence of steps that would get you there.
You don't have to figure it out yourself
and you can just see, oh, it's obvious now.
If it weren't for that line in see, oh, it's obvious now.
If it weren't for that line in the protocol,
then it's possible that like this set of things could happen
and then the protocol would break because, you know,
some constraint wasn't there or something like that.
Yes.
And then you can use that for tests
on your production code.
So even if you're writing tests, you know,
for your implementation, I don't know i sometimes it's
hard you know to come up with scenarios so how can i set up my environment in the test to reproduce
these scenarios uh quint can also help with that you just ask quid for a trace that hits the scenario
quint will give it to you or if you don't want one trace but you want ten thousand also easy it can give you amazing okay so we'd started talking about um i sort of forget where
we were we got distracted by traces you were saying they're your favorite thing we all we got
all excited um i think we were trying to talk about yeah oh we talked about the soup right and
how yeah yeah and that's also something interesting that's related to traces. Cause when you're using the right techniques,
for example, there's like looking at the message soup,
then your traces are smaller.
Not only your state machine.
So if your state machine is smaller,
usually means that also the traces are smaller, right?
So when we were talking about like receiving a pre-vote,
then another pre-vote, then another pre-vote,
and then you actually do something interesting.
This means you have to scroll to a longer trace. longer trace well if you just oh here we had quorum and therefore we meant we did
that this is much easier to read on the trace right also makes that right so these abstractions
we're talking about with the message soup that are built into choreo they actually make working
with traces a lot easier and if traces are one of the most valuable things you get out of Quint
and that helps you understand the protocol,
having good traces is actually very important
because if your traces are thousands of steps long,
it's going to be way harder to make any sense of it
and the value of the trace is going to be sort of minimal.
It basically becomes as if you're scrolling through the logs of your implementation and you see, you know, the debug logs basically, you know, one message at a time.
You kind of can't make sense of things because it's too much, right?
And so you want your traces to actually be small and full of useful information.
And so this message soup technique actually allows that to happen.
allows that to happen is that right yes yes that's right and i guess we can continue on traces
Is that right?
Yes.
Yes, that's right.
because this will lead uh oh yes sorry i got distracted uh yes we let's try to talk for 10
more minutes and then open the q a to the audience and then uh if someone has questions just write
them down and we'll get them to them in 10 minutes.
I want just to continue a bit on traces to get to my favorite thing maybe about choreo.
I don't know.
I have lots of things that I like, but traces are really like, because why do I like traces?
Because when I try to understand tendermint, traces were the most helpful thing for me.
So it made all the difference.
And with Quint, one thing that we introduced that were, was not on TLA plus.
So Quint is very compatible with TLA plus, like everything on Quint transpires to TLA plus,
but we have one extra thing that's not present on the TLA plus and it's not part of your state
machine.
It's not part of your spec.
And we call them like tests. They are sort part of your spec. And we call them like
tests. They are sort of like quint tests, or we call them also run. So you can use the keyword
run to specify a specific trace in the quint code. So in your code, you also write this,
as you would write like unit tests for your implementation, you write this runs for quint,
if you want. They're optional. But those are a way to bring the traces
to be sort of like first-class citizens
in your files and your specs.
These are not something just like JSON files you run
or something you save somewhere.
This can be part of your specification as well.
And when I was talking to Josef about this some years ago,
Josef told me like, this is way more useful than I thought, because these runs,
they are ways to document some scenarios.
So we were just talking about this, like super rare scenarios that
activate some super specific mechanisms.
You can, you as a protocol designer can document that to your, to the engineers,
for example, that are implementing the protocol for you or for the team.
And, but even not as a protocol designer, even like someone like me trying to the engineers, for example, that are implementing the protocol for you or for the team.
But even not as a protocol designer, even like someone like me trying to understand a protocol that I didn't know, like Tendermint, writing these runs from traces was really insightful.
And with Choreo, the way you write these runs are amazing.
It checks more things than you'd normally check.
It drives you to write
something of really high quality. And this is what I'm calling the cue pattern. And this is a
bit dance-oriented as well. So as we had the choreo nomenclature, I came up with this cue.
So you listen to some cue and then you do some some step in your dance, you perform something, right?
So first you have to hear your cue.
You are not going to perform something out of the blue.
Just as in protocols, like your node doesn't spontaneously decide to pre-vote, right?
It reacts to something.
So the cue is the thing you react to and then you perform something.
And when you write both your specification and your traces,
your runs like this,
it makes so clear what the protocol is doing at a high level.
So this is something that came later in the choreo.
So we already had choreo.
And then I was trying to improve the UX.
And then I came up with this queue pattern.
It's optional.
You can use choreo without the queue pattern if you don't like it.
There is a separate documentation about the queue pattern. But using the queue pattern basically means that everything you define in
the protocol has to have a queue and a perform step, what you actually do. So you have to define
when is this going to happen, reacting to what, what is this reacting to, and then what do you do.
into what is this reacting to?
And then what do you do?
And then your main,
because you have what we call a main listeners,
kind of like a main function in your programming language.
And you have like, when this happens, then you do that.
And if you look at the Tandermint version,
it's just so pretty,
because you have like, oh, when there are enough pre-votes,
then you do pre-commit.
When there is this,
so you can understand the protocol reading like seven lines of code in a high level.
And of course, if you want to understand what's actually happening in detail,
then you go to definition and you see what's in there.
But just reading the names is so good.
And then writing the traces is very precise.
So at this point, you use this like reaction, this cue, to see that this message arrived
or this event arrived, and then you performed this action.
And then after that, there was another reaction that performed an action, and then after that
another reaction.
And so you can be very precise to what actually happened, and it's amazing to read and understand.
Amazing.
So it sounds like really Chore like really choreo is just the
accumulation and synthesis of good modeling techniques that we've learned experience
developed over the years from actually writing, you know, a number of distributed system specs,
working with them, implementing them, debugging the implementation, trying to understand the
protocol. And we've just wrapped all that into a nice package called Choreo
that makes it easy for others
to write distributed system specs
without having to go through all those learnings
from scratch and just inherit
the sort of experience we've accumulated.
Yes, yes, I really hope so.
We need to get some new people to use it
and tell us what they think.
But I'm super happy with all the specs that we rewrote
in the pattern. I think every single
one of them looks so much better.
And I'm excited about rewriting more specs in Corel.
I think I want some vacation time
just to do that.
Which specs did we
rewrite in Corel?
We have four
official examples. Two-phase commit,
Tendermint, the Appenglow,
which is the Solana consensus and Monad BFT.
Right.
And then there's also the Minimit spec.
So the Minimit spec was written externally
from some amazing people.
And I think Dennis wrote that with someone else
from CommaWare.
And we actually got,
we have sort of like work in progress version of that it's
not published yet but we have a version of that with choreo and it looks really great uh i actually
that i didn't tell anyone about this but i was playing with writing amalekite spec for with
choreo yesterday uh and yeah i i'm i don't know i really like it i hope a lot of people like it as
well especially the people who want to try queens but have had like trouble feeling like the lack of batteries included experience and
like got stuck maybe at the message passing i hope choreo can be useful for them right okay amazing
anything else you want to say or should we open it for questions
no we can open for questions i think i think we got all covered and
if i didn't cover anything there's everything's own documentation uh and you can also ask questions
we have the telegram channel uh and i'm always available there to answer questions i really like
interacting with you all there uh so you can join the telegram channel we have a slip channel as
well if you prefer that, or everywhere.
GitHub as well works.
We have GitHub discussions where you can post questions.
But we have time for questions now.
We have 15 minutes.
So if anyone has anything. Do we have anyone here that's written a distributed system spec,
either in Quint or in another language,
and has, you know, battle scars to share?
Or are we all just curious about Quint
and, you know, planning to in the future?
One question.
Oh, go ahead.
Thanks, Gabriela.
Thanks, Ethan.
So I have some experience with Quint. What would be the best set of examples to try out Choreo?
Of course, I can read through what you have already, but what would you recommend as beginning
with Choreo examples?
So you want to write one example that doesn't exist in Choreo?
Yes. Yeah. I would get some of the textbook examples. Like we can maybe do Raft,
Paxos, one of those. Because I did two-phase commit and I had so much fun. So I think those
text books... So those are... Most Paxos and Raft are more complicated than two-phase commit.
But I think those can be very interesting.
And you can already find TLA specs or Parpaxos.
We even have a Quint spec that have,
that use already like sort of the message to pattern.
So it's easy to transfer them into Corio.
Or you can start from papers as well.
For I guess consensus algorithms have been the ones that we tried the most.
So grab any consensus algorithm, grab the paper, try to write a core respect from that.
That's interesting.
Cool.
Thanks.
And if I may go with another one.
Yes.
Go ahead.
So what I was wondering is, you mentioned the message soup technique.
Is there a way to introduce some assumptions on the soup?
Like, for example, I don't want message reordering or something like that.
So I have some external assumptions that I would like to introduce there.
Yeah. At the beginning, we thought about having those sort of different setups.
We didn't find a strong need for them, so we actually ended up not adding them to Choreo.
But if the need arises, we can add them.
I guess right now you would have to change sort of like the Choreo structure to represent this differently.
Or maybe adding some timestamps to your messages also works,
but you basically would need a different version of Choreo.
So we already have some different constructs inside Choreo
that can help you with different setups.
But for the messages specifically, we haven't added this now,
but we could have Choreo with sequential or ordered messages.
So then you represent your messages with a list instead of a set and
everything else stays mostly the same.
Right.
Thanks.
Some other questions or even comments, thoughts,
that don't have to be able to speak soon.
Just give it a second.
This space is a bit unintuitive for us.
We need to tell people
how do you, what do you have to press
to want to speak.
I don't know
because I've already chosen to be
a speaker.
No, yeah.
If anyone is struggling with the interface,
there is a button in the upper,
or sorry, the left down part of the spaces square
where you can request to speak.
I think there's a mic in there, but I also don't recall because I'm already speaking.
I think there's a mic in there,
but I also don't recall because I'm already speaking.
I've accepted the request a couple of times and it's not coming through, but I'll keep inviting Daniel to speak.
We'll see.
We might need Elon to approve him.
Yeah.
You don't have Elon's number?
No, I don't.
Shame.
We do have in the call here, or in the spaces here,
Yasin and Yosef, who were our main part of this development.
I think I forgot. Oh, no, I did mention that Yasin and Josef, who were a main part of this development.
I think I forgot.
Oh, no, I did mention, right,
that Yasin wrote his master thesis about this,
about choreo.
So, and he was the one who developed most of it.
And so if you want to check out his thesis,
he makes very, like, stronger arguments. So I'm explaining things kind of informally here,
but his thesis has, like, the proofs and stuff for how this,
especially how the message technique,
the message technique is great,
and also how you can extend choreo
and use it in different ways.
It's out there, so you can check that out.
And then I was going to say,
if Yasin or Josef want to say something, also feel free, please.
Yeah, I'm jumping in. I hope you hear me.
Also, because I have a hidden channel with Daniel and we chatted in the meantime, so I might guess his question.
He was thinking about the specific scenario in Malachite,
and it's sort of hard to find with the message-for-message semantics.
So he would be interested to see, because you mentioned that you're on Malachite now,
how far we are in this spec and whether we can look at special a special special semantics and special scenarios so uh
just to make sure i understand correctly so it's a scenario where the message by message would
catch it and no it's too long to catch it uh it's too complicated it takes so long yeah yeah yeah
that's interesting uh yeah i i would be definitely be definitely be very excited to rewrite the Malachite spec in the Choreo framework.
So what I tried yesterday, to be honest, I was thinking about some Malachite stuff and then I was like, oh, I'll just leave this running in the background while I'll do other stuff.
And I asked Claude to do it. And it's very interesting to see how it does it.
And I think it got a lot of things correctly.
And looking at the spec just seems very organized
with the queue pattern and like when this happened
and that happens, it looks really nice.
So I can share that with you and Daniel as well,
if you want to, oh, Daniel can speak, I guess.
He's speaker. Yeah, Daniel can speak, I guess. He's the speaker.
Yeah, I hope I can. Hey guys, how are you? Yeah, I don't know much about consensus protocol
itself, but I was wondering, asking, one thing that's hard to know when you have BFT protocols
is the behavior of Byzantine agents. The typical modeling that we do essentially produce all the message possible by Byzantine,
like every round, every value, etc., to try to emulate the attacks that you can try.
But this increases a lot the space, right?
Do you have some solution for that?
Because, I mean, you are around one, you have four messages generated by legit process,
and then you have 200 messages generated by Byzantines.
Yes, that's a very good question,
because this is where the message soup technique shines the most.
So I really recommend that you take a look at the message soup blog
that we posted on the Quint blog,
because we talk about
this there but uh so if you're not thinking about byzantine messages if you just have the the
regular ones then what we were talking about here with etan and having the messages in different
orders it has some impact when you add byzantine messages which as i said is usually such a larger
set than the good messages because there's so so many possibilities that what people can do wrong,
right? What, what the malicious, uh, wrong nodes can do. Uh, then the, the
difference that the message soup makes is huge. So think like you're in one node
and you have to consider like receiving all of the individual messages. If you're
doing the message by message style,
then you have to consider receiving
all of these different messages.
So three of the correct ones, 200 of the Byzantine ones.
So the chances that you pick a good messages
in random simulation, for example, are very low.
While if you do write them using the, like,
looking at the message soup and
observing if you have threshold,
you see how this problem
mostly goes away. Because you're
looking at the message soup and you're saying,
like, do I have quorum of pre-votes for something?
And then the Byzantine influence
there, like the,
how much it influences your state space is much
lower because the interesting
things that you do are much more on the correct messages than on the Byzantine messages, because
you have a bunch of validations, right?
So you're not going to receive any Byzantine message and do something about it.
Most of the Byzantine messages won't cause any reaction in the system unless you somehow
have quarrel.
So it does help so much with that factor as well.
Also, let me add that,
I think you mentioned it before,
Yassin has written a master thesis on this,
and he's called it now,
but he's actually on well-deserved vacations
after he's finished his thesis.
And he has done a lot of experiments,
performance experiments on Quint and also for Byzantine notes
in his thesis to take a look there. And pretty much shows the
graphs that he has there show that there's basically roughly no
influence or constant influence when you have Byzantine
messages in the message soup. While if you have this message by message
semantics, it
makes the traces very, very long. So it's super interesting to see the graphs. So yeah,
go there and check out this thesis also. A lot of data in there.
And with Choreo, it's super easy to interchange both as well, if you need to have both. Because
I know from Malachi, there are some things where you want to consider message by message.
So with Choreo, it should be super easy to have, some things where you want to consider message by message. So with Choreo it should be super easy to have,
like now I want to run it with message by message semantics.
Oh, now I want to run with message sub semantics.
So it should be easy to have both.
Yeah, I remember.
There is another thing that I think some you have mentioned
in the presentations that regarding message loss.
I had a look on the code and apparently the message has a sender, right?
But it doesn't have a destination.
So when you have a message loss, the message is lost for everyone.
Am I correct here or I interpreted it wrong?
No, because so the message is never taken out of the set in that sense.
No, because so the message is never taken out of the set in that sense.
Yep.
What can happen is that a certain node never receives that message or never
receives that message.
So when you are looking also at the set of all messages that the node sees,
you can not look at the entire set.
You can look at a subset of that.
So for node one, you'll see all messages, but for node two, when you're going to
like do the message sub technique, you're going to only see a subset of the messages. You can do it
like that. So you can program as a, okay, a message can be seen by some subset of the processes,
because again, when we are talking about Byzantine attacks, this is super important, right? The
ability, for example, of sending a message to some guys,
another different message to others, right?
Yes.
Yeah, I'm a bit too short.
So what I just told you, it's not the best,
like the most performatic thing,
considering all subsets and stuff, but we do have,
so if you look at the Tendermint spec in Corio,
we do have a run for disagreement where this happens.
This was just said, like the,
you see some messages from one Byzantine
and the other processes receive another message
from the business.
So these are the receiving part of the code.
It's not on the sending.
The sending is done for all,
and the message is always there,
but you can non-deterministically not receive certain message.
Okay, great.
Yeah, I think it's something that we,
yeah, we have tried to do a generic network.
I think I even discussed it with you
because this is looking super important to me
to have a generic network layer to say like that, right? Because for every protocol, you have to write this down
again. And I think this is very useful. I tried to read the masterpieces, but it's very mathematical.
It will take some time to understand all the formulas, but very nice work. And yeah, I hope
it will be useful for you and also for other people that are designing
products.
Thank you, Daniel.
Thank you for your feedback.
Yeah, and the master thesis is more like if you're going to go deep into the mathematical
part, but if you just want to use Choreo, I recommend you read the documentation that
we have on the website.
So on the Quint website, we have Choreo tab, and you can check out the more like practical stuff in there.
Okay, we are about time,
but if anyone has one more question, we can do it.
Otherwise,
I'll give you 10 seconds to ask for to speak.
Then Ocean can let me know.
Maybe just a closing question, Gabriela.
You said traces and runs are probably your favorite features of Quint.
What's your favorite spec that you've written?
That I've written. Or not, that you've reviewed.
Oh, it's tricky. I think I fell in love with the Tendermint one for a while. Because I
have written I think so many versions of it. Like we had a very initial version that is
very close to what we had in TLA
because we had a Tendermint spec in TLA and then we just
made like a kind of like direct
translation to Quint and then that spec
kind of like evolved and I've written a different
version. That's how like the first
experiments on choreo was also done with
Tendermint from my side
and now we have this choreo
spec that I really like it.
I want to show it to everyone.
So I think that that is my favorite.
Very cool.
And for fun, I really like the tic-tac-toe example.
Okay, great.
Awesome.
Well, if there's nothing else, this was great.
Thanks, everyone, for tuning in.
And check out Quint and check out Choreo.
Yes, thank you, everyone.
Thank you for listening.
Bye, all. Thank you. Take care.
Bye-bye.
