Formal Verification of Consensus Protocols in Lean

Transcript

Thank you. Thank you. Um just a bit of an introduction. Um Alberto. I work at the Ethereum Foundation as a researcher on consensus protocol. I've done before joining the Ethereum Foundation, I was at ConsenSys where I did quite a bit of work on formal verification of consensus protocols and distributed systems. Uh the tool I used back then was Daphne, which is bit different from Lean. So this a lot of this workshop or talk would be uh general in a way on how to techniques and what we need to look for when uh

formally verifying distributed systems. So there is a bit of Lean into it, but as I said it's a bit more high level than just Lean. So I'll start with a temperature check in the room. I just want to understand by raise of hand who is more of a formal verification person. Okay. By raise of hand who is more of a distributed system person? Oh interesting. Cool.

Um okay. I don't need to go over the other two intersections. Um okay. I start with uh as a as um introduction. Feel free to interrupt me at any time. I want to keep this uh interactive. I've a lot of slides and I can make the presentation or the workshop dynamic depending on where what things you like to ask and what things you want to dive into. Um so feel free to jump in at any at any point in time.

I wanted to start with explaining is important to get right. I think it's given the amount of people that are more on the distributed system side of things. I think this is quite important as I think formal verification people already know about what I'm going to say here. So the most important thing you need to really get right are two things is how you specify the model and how you specify the statements. And this is the trusted part which is uh what you need to read carefully also you know that is any formal verified project or anything that is formally verified or

what is formally verified is statement against the model. That's what is formally verified. So just to put in into pictures you especially in distributed systems we'll see later how we can model the the the the environment. But assume that you have this is like a set and in the green box assume you have the possible different executions that you have modeled.

Now if there if there are executions that can happen but outside your model doesn't matter what properties you have proved on your green model you haven't proved anything on on what it doesn't is not covered by the model. And modeling things especially in distributed systems think is not that easy. There are many pitfalls. Um I'm I'm not a cryptographic expert. Um I think it's in terms of uh specification of cryptographic functions perhaps it's less likely say someone can correct me in um

in following this problem mainly because you don't have concurrency, you don't have different uh nodes acting at different times. So the model is really how you schedule events, how for example, this is an example, I say that your model just deals with integer times. Well, reality doesn't have integer times, so it could be an execution where many actually where you have real time and these executions are not captured, so you're not expressing you're not formally verifying those executions. In this case, you'll only be formally find those that have real time.

So this is why it to be it is important to to write a real model that models the system the environment as as close to reality as possible, but also to check for any formal verification project that the system has been correctly modeled. And the other, as I said, that important thing to really um get it right are the statements. So this is probably more intuitive. If what we prove is in the green circle, but what we intend is in the in the blue circle, so if what we have our statements cover only this set,

well, we we have proved this set, but we have not proved what we really want. Uh so again, I I stress it's important uh in terms of modeling statements, we trust them. Lean is not going to tell us whether they're right or wrong. This is something where we need humans and think this is also a good argument for why we are still relevant in this AI era. We need to really uh check um these trusted parts of the of the system.

There are things, for example, the I can so that the link can tell you, for example, you could say that, you know, you specify something that exclude all possible executions, but won't tell you whether again, the model is not the one that describes reality or statements and not those that you intend. So these are very things very important to to check on any on any project. So again, again, uh about checking model specification, theorem statements, then if you have a project, I suggest you download and and and run uh linear self so to make sure that it does actually check the proofs.

And there's a we could print axioms like in Lean you can have um you can say for example, you can use a prove by sorry, which means basically the the the statement is is assumed to be true without a proof. And so it's important to check with with axioms are used to make sure that there is no such a proof or such a proof is actually uh might not hold it, which in this case if your your if your entire uh project relies on such a statement which is false, um you wouldn't get any guarantee.

Then I wanted to go over um I mean are there questions in regard to this session? Yeah. >> The idea here is to >> um >> Can you repeat the question so we get it the mic? >> Uh sorry. Yeah. So the the question is understood it um is about whether this is about um when you write the specification or actually trying to prove a real system.

Um so in this what I've in what I've been on the screen now is about writing the specification. Um that's where you start from. Um if you want to prove a real implementation, there are questions like what what language have you used for the real implementation? What probably won't be lean, so you need a way to bridge between that language and lean, for example. That again is a trusted part, but if you if you have a tool and the tool is correct in terms of translation, then you can show that your translation complies with the lean specification that so the specification is what first

you need to get right. In your case, what you need to get right is the transpiler. And and that and you need that's what you need to trust. >> Um but is there a problem where like the model you write with a specification which is simplified because lean we can't model threads and concurrency or networking even? How are you transpiling your implementation into lean basically is my question because you you you can't what your implementation is talking about is talking about networking and stuff like this, but that doesn't exist in lean so your specific like how can you prove equivalence between these two things which live in like different worlds?

>> Yeah, when if you have something that does multi-threading, in theory you need to basically translate every routine and model the concurrency which you can do. It becomes very like you can do it, but it becomes very complicated because you also need to model the concurrency which you can do of the multi-threading model. So you need basically to transpile every routine that and then model okay this can happen in this thread, this can happen in this thread, and that can happen concurrently.

It's it's not that different from a distributed system. So basically like it's I know that rather than being an atomic unit, you can decompose it again in threads. You can use the techniques to do. Okay. Um, so I wanted to go over a bit of the distributed systems modeling problem we have. Uh, first thing, um, the we have a non-deterministic system. This is because you have a network, messages can be delivered at any point in time. So if you start from this state, you can go to four different worlds, for example, just to mention a few, depending on which message is received.

Like if it's if if now if now V three receives M one, we are in world one. If V one receives M two, we are in world two. You can imagine there are many, many, many worlds like this. And I know if you are aware of other formal verification techniques, um, like model checking, model checking, what you do very in a simplistic way, you start from a state and explore the different states that you generate from that. And generally model checking has limitation expected except uh particularly when you deal with uh distributed systems, so system where you have

probably potential arbitrary behavior because you have an explosion of states, but what we can do with theorem proving, we can actually deal with all of this because we kind of express overall properties that are true regardless of the ordering of the messages. But this this non-determinism is something that if you are dealing with cryptographic functions that the nation is not something you need to worry about. Again, as I said, like other sources, non-determinism is given by Byzantine nodes, the nodes that don't follow the protocol, they can do anything with limitations. They can't change another node state, but they can relay relay any messages. They can sign with

their own keys any message at any point in time. So you need to the model must allow for this. Then we have other other questions. We need like to to be able to model different type of network conditions at at at this uh and they can change. For example, we need usually in distributed uh protocols we have this concept of partial synchrony. When messages there is this time called global stabilization time. Before then mess we don't have any bound on how long it takes for a message to be delivered.

And after this GST you know there is a known delta uh and messages are delivered in within delta. Again not don't want to go too much into the details necessarily now, but I can if you want. What what what I'm trying to to convey is that we have we need to be able to model this type of environment. We also need to be able to model nodes that fall asleep or crash. This is something that can happen. They crash and they restart.

These are all problems that we have. Let's say that I think are quite peculiar of distributed systems and in a way this is what in my opinion makes quite tricky to get the modeling on the environment right. And I think that's what yeah that that was kind of the point I was trying to stress in the first section. Generally there are two types of properties we are interested. One is safety which means um nothing bad will ever happen. For example, you can never finalize two conflicting blocks.

So, you show that that can never happen. The other thing is showing that something good will eventually happen which is that you eventually finalize a new block. This is just to give an overview. Are there any questions this? >> If you have any questions just raise your hand or if you don't want to speak in the mic, you can also ask a question on the app. >> Cool.

Okay. What I'm going to do next, I'm going to give you an overview of this general framework and how it has been put together that is that I think is a good framework to model a real system. So at the moment, this is the framework and this is currently I'm applying it to the couple consensus which is an improvement on the current Ethereum consensus protocol where we the couple timelines.

This is a draft branch. I'm actively working on it. I'll expect some major release in a couple of weeks and I'll I'll share it on the Telegram chat. So be free to to head to that link. But just have an overview, but anyway, there will be an update in two weeks. But I'm going to focus more is about the framework which I think is pretty stable. One thing I'd like to stress out, you'll see a lot of details potentially and these details are needed to to be able to model accurately a system only if you want.

I mean, that's the key. Like you can really, as I explained later, you can start having a very simple model where you say I have just one shared clock. Every every node ticks exactly at the same time. You can have just honest validators, perhaps no crashes. And then you can start adding level of complexities. For it you can start dealing with crashes, with Byzantine nodes. Um And and what I'm trying to convey is that you'll see a lot of details, but you don't necessarily need to think about all of the these details at the beginning, but the framework must allow you to express uh any behavior if you want to eventually

expand it, expand the model, expand what you're trying to formally verify, and also to extend the level of details of the properties you're trying to formally verify. So one element you have a schedule and the schedule determines who is awake, who is adversarial. Um Okay, here you have integer numbers because this is the node slide for one the model was dealing with with integers, but this actually can be they actually can be real times.

So saying from this time to that time um for example in this case from from time three to time four nothing changes. At time four this validator becomes corrupt and and then at time seven uh this corrupt and then potentially you can go back to being honest. Um the idea is that like you have a very what you want to do, you want to have a framework that allows behavior that perhaps you are not willing to accept.

For example generally we don't want to deal with uh validators to become honest about after being corrupt because it is that once you're corrupt then there's nothing you can do even if you can't really become honest because while while you while you are corrupted, someone else stole your keys for example. But it's good to have the framework that allows that and then you put constraints. So you say this is something cannot happen. Then the the element is how the the system evolves.

So what you what you have is a state which is the state of the entire system. You have for each for each nodes you have uh state of the node, the clock, the set of messages that have been received and the state of the node. And then you have a state for the network with all the messages that have been sent. This is just a modeling uh technique. Clearly the state the network doesn't keep track of the messages. It's not something that is stored there, but you and you don't allow the nodes to actually know what this uh set of messages that have been sent are, but this is just a

something you need to keep in order to express properties. For example, you can say uh a message that was sent at time T will always be delivered by time T plus X. And to do so, you need to keep track of uh messages, for example, in the network. But again, this is just a modeling feature. Then how do we evolve? So we evolve from one state on the left to the one on the right based on an event. In this case, say uh V2 uh V2 receives a message M1 sent signed by V1, for example.

So we go from the system state to this system state. What it changes is that um the state of V2 is updated because it it has received a message that something updates its state. Uh the the message is added to the set of messages that have been received. And also V2 might send when they decide to send a new message. So essentially you have a function that gives you two outputs at least. One is the new state and the second output is the center of set of messages that the node will send as a reaction to an event.

To make things a bit more realistic, there is more to it. For example, there are the input output are not only messages that are sent but actually things you write to disk. And things you write to disk can be decomposed in in in as many details as you want. You could decompose it to byte depending what is the atomicity of the of your say permanent storage system. So for example, you can have it's not represented Yeah, for example, you you could have different type of this is the two will

be representing something that is written to disk. And so like the output again is not necessary only set of messages, but it's also the set of operation you perform on disk. In terms of steps, these are generally the steps that you have to evolve from one configuration to the other. And go So you have environment steps, adversary and specific steps that a node will take. So one of the step is you the clock moves. This is the wall clock.

So generally the framework allow you first set the environment sets the clock. Then all sort of events happen on that that clock time. And that allows to that allows to to model things like immediate message delivery if you want to. Like you can have delivery of messages in time zero. You can also potentially then have they say that you have you want to consider a system with parallel processes. You can have potentially at the same time two events happening on the same node because the node for example has you know is splitting two parallel systems. And so because of this it's important that the framework allows

many events to happen exactly at the same time even though that is a real time. Um there are another event is corrupting a node. A node can become corrupt. The crashing so the environment decides when the node will crash. Then this is about the node can also decide they say that you have different operation happening because of an event like you send a message, you write to disk, you send another message.

The environment can say okay you crash exactly you might crash after you on the second operation. So in this way you can basically model something where your you get to some sort of corrupted state. So you can model a system where basically you know say you write two values to disk and the the sum must always be five. Well if you don't do that carefully that might that might be broken. So the model does allow that. Um as I said before it's not something you need to deal with it immediately.

You can just assume this never happens initially and then you you refine down your details and you deal you you're trying to deal with this increased level of complexity. Another another event is about the starting so you when if you in a in a real system when you restart some of the um state is persisted which is the disk and some of the state in memory is um is zeroed or starts from some arbitrary state. So the model does allow that allow to to say when you start some of the state is persisted and the other and the some of

some of the other state is not. There is a tick event which is represents basically a sort of interrupt from the system which says the system has advanced to this clock time um and you can express this to be like a skew compared to real time. You can say the clock time is always updated within you know half a half a half a second of the real clock time. So in this way you can actually model skew skewed skewed clocks. Then you have delivery which is receiving a message.

Uh this is just a custom event. And then you have the adversarial. So what the adversary can do in generally um the adversary can um uh let's look at the second row. The adversary can send any sort of messages. Uh there are constraints for that you can put on the system which is the adversary can never send a message signed by um an honest node except if that honest node has already sent uh the message. And so that in this case the adversary just Now as I said in the beginning that is an important

I might stop here actually if other questions on this topic or what we have seen so far. Taking that. >> You have a question? >> No. Cool. So as I said one um all of this modeling allows for a lot of non-determinism is that you can move from one configuration to possible different configurations based on uh what the environment do. The environment decide to like to deliver some messages and uh according to the message you move

to different states and then from there you move to different states again. So this is something that the model allows. An important feature, I think, that you you can have is also not only have non non determinism in how the overall system progresses, but actually have non determinism in how a node responds to an event. So you can imagine that you start from a state, you receive an event and you allow a node to potentially do three different things arbitrarily.

What I think what is nice about this is in a situation like imagine what we have in Ethereum mainnet, we have a spec, but clients can potentially implement the spec in different ways. So in this way you can actually and we always have this problem where clients say, well, I want to do my own optimization or for example, I want to deal with the queue of messages my own way. And they in a way they want to do things differently. What you can do, you can actually model. You can say, okay, all of these behaviors are allowed. You can pick and choose the one you want. It doesn't matter which one you you you you choose, these properties will be guaranteed. In this way you can allow to the implementers freedom or not they choose to do and how

they choose to deal with some freedom, but at the same time prove that that the protocol is correct as long as they abide to some bounds, which you for example you can't do today with the Python specification which says you need to do exactly this. But that means that as soon as you do something different, what you've proven is not proven. >> There's a question on the app now that does modeling require heavy mathematical background? >> I I think it does require some mathematical background, yes, in logic.

It if are on today with the AI and LLM tools that makes it a bit better, but as I was stressing at the beginning, the model of the system is what you really trust. So, you know, you can generate code through LLMs, but you really need to check it. So yes. It has required though if if you're willing to trust, let's say, say a framework used by many people who are in the case yeah, you trust the authors, you trust the people who are reviewing it and and using an existing framework requires less probably less mathematical expertise.

>> Yeah. Uh, under this model, do you make assumptions about the network itself? So, like say I'm an honest node, but the network applies some error to my messages or my yeah or >> Like your your message might get corrupted >> Yes. So, it's is that just bundled bundled in with a corrupted uh, node or like do you have this notion of an honest node but let's say with a malicious or error or a network with error? >> So, so far I don't have a I don't have the notion of network error.

Um >> Do do you need one? Does that matter Do you care about this at all or not? >> Yeah, yeah. That's a good point. I don't know if you can express it. Um I think you can express it because the yeah um It's a good point. I think that's something probably worth considering. Like you could Yeah, at the moment you don't have it because you describe what honest uh, notes Well, I assume you could add it here because you could have like a spec where you say this message it can be sent and one of the messages potentially is a corrupted

one. So you could model it is already sent as corrupted rather than it's corrupted on the way. Yeah. Yeah, potentially. But I never I haven't thought about this so yeah. Thank you. That a very good question. >> There's no more questions in the app. We can for example take the first one. Can we also model conspiracy between adversaries? Subset of validators do some X Y Z to corrupt the chain.

>> Yeah. Yeah. Yeah, you can like in a way we have a sort of conspiracy between the serial node like any Byzantine node can do anything that any other Byzantine node can do. But I think this question is about whether you can do something that is not completely wrong but you do something like timing games or I don't know. You're trying to gain some advantage, some economic advantage. A Duke can model that.

It's not something I've thought about how to model but you can model it because again you can have you can have a sort of a bit or something that tells you in the initialization. For example, you can say you can have different type of honest nodes. So like you can in a way specify what honesty is per type and one of these honesty honesty is could be for example you try to employ in timing games you're trying to divert a bit from the protocol. So yeah, I think it can be done.

>> Then there's also a question that do Do model dishonest behavior and allow other combinations to be valid, or do we need to model for specific cases with constraints? >> You need to model specific cases, yeah, or specify them, yeah, one of the two. Um so as the framework comes at this stage like you just have adversarial and honest, in a way this is um a convenience. They said before like you could think of having just honest nodes with a type and because honest nodes can have

non-deterministic behavior essentially, adversarial could be a type of node which allows anything. So in a way the framework makes it easier to say this is adversarial, this is honest, that can be extended to allow yeah, what what the question asks. >> And then there's kind of a follow-up question that with all this like complexity, is there a point where where formal verification just says that okay, this is just a model and we won't have more complexity? >> It's a good question. Um didn't have an easy answer.

I probably there could be a point uh definitely there was a point before we we had this uh advancement in LLMs like just two years ago for example even proving liveness properties was a headache, uh something that nobody was doing because it was just too complex. So I think with the in the era of AI and LLMs we can really push the boundaries a lot and and push the envelope um in terms of level of details. One thing I'm thinking about is the say you want to model a network with some probabilistic distribution of how

messages are sent. That could be quite hard problem like you might not be able to actually come with with bounded probabilities, so there could be a limit. Um. But I don't know. It's in theory there is a limit where you have you have basically just express your your node as assembly with multi-threading. I think I think there is a point where basically becomes the cost becomes probably too high. Makes sense.

It it's hard to say where the point is though. Any Okay. >> There's also a question that for some of the audience that is still like new to this topic. Is there some like getting started guide for formal verification like generic one that you recommend people to read? >> I think in my opinion there there are nice ones for Daphne written by the the the creator of Daphne it's not a lean.

That I can if people are on the Telegram formal verification chat for the can share the sources there. That is the one is it covers for example some of the concepts about modern distributed systems with Daphne and not with lean and then there are lean tutorials. There isn't a one stop website or guide or Okay. All right. Keep going.

So I use case for example non-deterministic honest behavior let's say this is very simple they said that they received a set of votes. You need to pack them in into a block. You can a block is a list you can decide to pack them in any order you want to show that the protocol is correct. This is something that is probably say obvious but again if you want to have a really formal verified system, you want to show that it doesn't matter how you order messages. But potentially you can have a bug where you say I don't know, for one reason or another, your your your your implementation you read the first X and some ordering always always allows you to to

for example to satisfy some property and another order it doesn't. So this is like a simple but just to give you an idea of an example where non-determinism helps in honest behavior as well. But I won't go over this, but this was to explain what you reason about digital clocks. Actually, if you don't do things carefully, you might not you might exclude systems when you actually move to real clocks. But this was a bit complex.

Um I'm going to move to modeling constraints. I'll go over this quickly as already um talked a bit about it. So just to give you an idea, I say that you have a schedule that allows uh any Oh yeah. I say that you have our schedule this schedule allows even dishonest validators to become honest. What you see what you have you have a constraint which says that this the set of of dishonest validators can only grow.

Um like this one, you say the set of dishonest validators at time T is a subset of set of validators at time T prime for any T prime larger than or equal to T. So you have these constraints on the model to come up with let's say a more simplistic description of the environment which arguably allow the simple for you to prove properties and then you can peel back these constraints. In this way you can have this kind of iterative progressive approach to formal verification where you don't need it's not a one or zero. You do formally verify some properties on a simplified potentially version of the and then you enriches your uh your set of properties or enrich the model.

Same thing for time for example but the model actually write time to progress at at any backward forward then you constrain it to be monotone same thing for unforgeability actually the model the framework as it is bare allows for um adversary to forge honest validators messages and you add a constraint saying that this is not possible. Same thing for the clock drift um same for list concept of partial synchrony you say messages can only be delivered um after say this GST they must be delivered in in in a some known time delta um something interesting for us

we Ethereum don't know if you know about it but we want to deal with want to be able to produce blocks even if you have very low participation in the network and we we need to model this regime where um some validate validators can be offline but we know less must bear that the number of honest and online validators are more than the adversarial one. Again this is something you model by saying you know at any point in the system the number those that are active or honest are more than the adversarial one.

And these are all let's say constraints that you are or you can peel back. Next thing I wanted to draw attention on was how we specify properties. Now what you generally have like if you model a client in Ethereum client you have a lot of state we are keeping track of uh justified of the justified block we are keeping track of of of all the votes that we have received potentially we we keep track of um slashing for example or other things but when you when you describe properties in

a way some of the state that you keep is just to state that you need the nodes need in order to know what to do next. But what really you want to to specify properties on is actually is on a view and this view you need to think like assume that you are an external observer just sitting on the network. This external view is the set of messages that are sent and for example you can have a peak in the in the state of the node and for example what you care about for example is the finalized state is the finalized block.

So what you can do to be able to express properties in a more general way you don't express the properties on the actual node state but you can express your properties on this filtered view which has less state it's only the state that you care about and for example which is the finalized block and the set of messages to be sent and and some other state. So in this way you can uh you can also say different implementations that satisfy these properties. Does this make sense?

Are there any questions on this? So if we look at um the protocol we're working on for example again we we have many many states and we just for what we care for example for some of the properties is finalized block which is confirmed and the blocks it holds and that's what we express properties on. >> There's a question how do we model liveliness with or without fairness assumptions?

>> We need well we need to mm have some fairness assumption there in order to uh model liveliness on fairness assumption is said that the clock will eventually advance that uh any honest node will eventually tick. We can't model liveliness without fairness assumptions. So that's what we need to express. Um one thing perhaps another question is about like we strong fairness concepts that uh um right well known informal verification.

I mean based on my knowledge that something like you have to have this concept of fairness about events and then you are which are well defined and you say if this is true then I can show something will happen. But been able to do um was actually to have a more say custom definition of fairness rather than using this more say general definitions and that's because in my opinion like before of we had access to LLMs that could build proofs yet to really trying to use some underlying theory that for example

that allows you to deduce conclusions from well known definitions. Well in this case for example I you know in a custom way I am expressing clock will eventually advance and then um LLM is actually able to prove that the conclusion holds. Think another interesting concepts is okay so you have a specified your model your properties great uh you build your proofs.

Now if you just let the LLM or the IBEX proofs for you uh eventually it will do it if your protocol is correct. But we come up with something very entangled something very monolithic. Now what's going to happen is that you are going to change a variable in your spec and that is going to change is to going take ages for the LLM fix all the proofs because the variable compares in many proofs for the lean to rebuild, re-verify everything. So even though we have access to LM and the AI to build the proofs, I think it's portal we would actually interact with the LM in how the proofs are written and structured. For example, it is generally

good to have like a an intermediate level where all the properties are expressed on this intermediate level and your specification is proved to just map to this intermediate level so that if you change the say just the variable, you don't need to prove everything or all the all the proofs that rely on the mid intermediate level are untouched only you need to change is to to change is one proof for example that shows that uh now you're using X rather than Y.

I think this is quite important concept in terms of especially of maintaining formal verification project like for example Ethereum where things change. Specs change is not something that is uh defined that will be like that forever. We need to be able to be quite flexible and lean now we keep the proof updated with how the spec progresses. So just to give you an idea idea you can think of two levels like you have uh the concrete what they call concrete is actually the actual specification and you have proofs.

So the proofs are um this proof level that you have a specification on a abstract model. So by abstract model I mean you don't say you don't go into how the function is decomposed in sub-function. You just describe input and output from menu for example receive a messages to the messages you sent. And then you build proofs on this abstract level. And then what you have, you have a bridge that shows that this concrete level implements the abstract level and then you show that any proof on statements on the abstract level

just you have what we have basically what you have we have one proof that shows that if if this mapping is true any anything you approve on the abstract level transfers to the concrete level and then from there you can any any statement is transfers automatically. And this is what allows to make proofs more robust to to changes. Questions on this? Yeah. >> So you mentioned previously optimizations um with the other use case I have in mind is when you have uh an implementation for example or a

spec really and then you have another spec for something else and you want to prove equivalence between the two for example you know a spec for a protocol and a spec for an ISA uh of some particular CPU and then you want to prove equivalence between the spec and the assembly code that you're you're looking at. Would would this be the mechanism or how does that work? >> Uh yeah it's a slightly different mechanism. It's uh about this which okay.

In this case I did for a different use case but so you can do this through refinement. Um the idea is that you just looking at this diagram what it's something sitting here. So let's say you have proved um let's say your your your spec and that's not written in assembly, is written in lean. Example, then you have your assembly, some assembly. You want to show that that assembly is a correct implementation of your spec, then it's something that sits here.

It will be here. All you have to do is prove that this assembly maps to the spec. Mapping means for any input if you process this input through the lean code or if you process this input from the assembly code, the output will be exactly the same. So and you you for example, you prove it this level underneath here. You can have this layering. Okay.

Okay. And this is a concept you can apply like you can initially have strong assumptions. For example, um one nice assumptions currently I have say that you have in Ethereum we don't process blocks that arrive too early where this compared to the current time. Um but we for example, because of skew time, we can't just drop them. Uh we need to keep in the queue and process them again. Now what you can do we initially we don't need to specify protocol that has this queueing mechanism. You just put the assumption a stage one in your network. You say

network will deliver the block again. You prove your properties and then you refine the model and now you actually put this queue mechanism within the code of the spec and then you prove this mapping. You you prove that the spec with this improvement with the but basically you show that if you drop this assumption that the network will deliver things for you again but you have a queue implemented in the code in the spec. This is equivalent.

This this will be stage two. This is equivalent to stage one where we had this assumption on the network. So in this way it's what is nice is that you can again think about level of of complexity in in an incremental way. Uh yeah, I think this this concludes the main part. Yeah, if there are questions happy to take or hand it over. >> So I think we're running out of time, but maybe you mentioned the Telegram group several times.

>> Yeah. >> Can you show people how to find the Telegram group and then you can continue asking questions there or share resources? >> Just not sure up. I was invited to Okay, well maybe just come and talk to Roberto after this talk >> and uh