# VLSMs—analyzing faulty distributed systems by Vlad Zamfir | Devcon SEA

- Speakers: [Vlad Zamfir](https://streameth.org/speakers/vlad-zamfir)
- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2025-10-07
- Duration: 29:49
- Watch: https://streameth.org/watch/yt-loyKzWQlyEo
- YouTube: https://www.youtube.com/watch?v=loyKzWQlyEo

## Description

Validating Labeled State transition and Message production systems (VLSMs) provide a general approach to modeling and verifying faulty distributed systems. With formal definitions of validation and equivocation, we are able to prove that for systems of validators, the impact of Byzantine components is indistinguishable from the effect of the introduction of corresponding equivocating components. All of the results presented in this talk have been formalized and checked in the Coq proof assistant

Speaker(s): Vlad Zamfir
Skill level: Expert
Track: Core Protocol
Keywords: Consensus, Distributed validator technology, Formal Verification, correct-by-construction

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum, https://warpcast.com/devcon
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon SEA was held in Bangkok, Thailand on Nov 12 - Nov 15, 2024.
Devcon is organized and presented by the Ethereum Foundation. To find out more, please visit https://ethereum.foundation/

## Transcript

[Music] testing testing hi everyone Hi hi um yeah I'll take this mic actually thank you for thank you for coming to this early morning talk um it's going to be a talk on formal verification and like basic methods in um distributed systems and reasoning about faulty distributed systems um all of the everything presented here has been formally verified by the uh team at runtime verification uh and is like available to like click and check uh and you look at the uh the proofs in but this talk is not going to be focused on the proofs more just definitions and theorems and um not really walking through the proofs um but you can check them out and there's a so I've separated an a bunch of sections a section on validation Theory a section on equivocation Theory and then on uh relating and uh reducing Byzantine faults to equivocation faults in the context of validators um so let's kick it off so let's talk about validation um and this so here here's the here's these slides are I actually a little disorder this so this is the this is the name of the paper uh um validating label um State transition message production systems um so it's for fault for modeling distributed systems faulty distributed systems and all these amazing people worked on it for a long time here you can scan this QR code and pull up the PDF if you like um I'll show this also again later so here's the validation Theory section outline basically we're going to go through this the definition of this model uh its compositions and then the definition of validator and then move on to the equivocation section so here's the first definition here um so of a vlsm is uh topple you know as we often like to Define these things um it's sort of like a state transition system like you're normally used to except for it has a few other things like the lab a label which is also not to unconventional and uh but it has a first order message set in the definition uh it has initial States and initial messages and then there's a transition function that takes labels States and messages optional messages and gives us States and optional messages this is like this State transition SL message receipt and production uh function that like describes you know for a particular VSM you know sort of what's Happening computationally uh you know you can imagine and then they're also equipped with another thing which is why they're called validating this beta which is a validity condition and it basically says when it's going to be valid to transition on a label from a state to given a message so when particular State and you receive a message and you know you might want a transition might multiple possible transitions each identified by a label um and some of them might be basically banned even though they're defined by the transition the validity condition won't let you take that transition so this is like a state transition system with Native messages with initial States and messages and with a transition uh like a transition I function that's you know totally defined over these over this domain and then and then we sort of restrict it effectively making it partial uh with this validity um condition this is like the validation condition basically we're going to imagine that these things don't transition even though the transition is defined when the validation condition is not satisfied um and so that's that's the definition but actually uh I haven't told you um uh sort of how to get the states and messages but you know it's sort of what you would expect you start at the initial states in the messages and then we build up this fix Point um by taking the union of all the states that you get from the Transitions and all the messages that you get from the Transitions and transitioning from those States using those messages so basically starting from the initial States and messages um transitioning and sending all them uh all the messages I've produced from there uh and receiving them and doing it over and over again basically until you know you even get stuff like a node in an early State receiving a message from some other state um uh this really is like a a big fix Point um and so so so there is an interesting thing that can sort of happen which is the validity condition um can be satisfied even when an input message is uh invalid um so we have to slightly distinguish between just this just the validity condition being satisfied and the actual Trace being valid the trace is valid only if uh all the input messages are also valid um so you know no no no no no garbage in sort of allow in a valid message so so so that's basically the definition of VSM and then they have a pretty natural way to compose them um and so now I'm going to go through that definition unless you unless someone has like a question now before the before composition okay so basically what we're going to do is we're going to take a disjoint sum of the components for the label so we identify the label which component is the state is a tle of the component States the initial States is a topple of the initial States and then the uh we have like a union of the messages for the uh for the initial messages um and then here actually we we're composing U vsms that have the same message uh type um this is just so that all so that all their transitions are are defined and everything and you know to let them send messages to and from each other they're not just uh independently like if that was a disjoint Union they wouldn't be communicating so we have a disjoint Union for the labels uh tupple for the state and then a regular Union for the messages um and then in the in the in the free composition we have a transition that basically just affects only one component exactly according to the transition that would have had before the composition and checks the validity condition only of that component exactly like it was before so very little uh basically nothing being done by the composition except for uh transitioning the individual components and checking their individual composition uh sorry sorry their individual validity conditions uh individually there's no composition wise constraints they but they but they but they can message each each other in this uh thing and then you know note also that this is also a VSM um and that's why it's like sort of a it's a composable model um you know same tople definition and everything yeah MH so the question is is the split up between the transition and the validity uh purely mathematical I mean I guess it's for the sake of convenience when dealing with the math and um so I but I mean uh in more more traditionally in math you would use like a partial function I guess guess whereas here we're we're about to get into this conversation about validation and um distributed systems and what can happen in a distribut systems that you might not be able to tell locally about and so it gets um there's there there is a reason why we are thinking about the validation at different levels and actually um and that actually does sort of spell it out basically there's going to be actually in the next slide um we're going I'm going to apply uh we're going to talk about compos constraint compositions where there's an additional constra constraint on the uh so basically like this constraint composition just basically conjuncts a constraint on top of the uh validity on top of the validity constraint of the free composition which just is the individual con constraints applied independently so this this this composition constraint um you know let us sort of analyze uh things a little bit more conveniently than just a partial function approach um um um yeah so the question is if we're doing this to try to see if a transaction is possible but not valid and yeah you're very much going the right direction um and uh we're getting there with this definition here so this is the def this is the def def definition of validator it's very natural simple definition of validator um which is kind of useful in many many different contexts um so in a in a and and so the components are a validator for the composition basically they're checking if they're truly a part of that composition or if they're like um and they're sort of you know only transitioning as if they are part of that composition even though they don't know it per se so let me just go through this definition so basically a component in a constraint composition is a validator if any transition that that component can make can be lifted to a valid transition in that uh composition so if the component has a valid transition then uh if if a validator has a transition which it can take then there there's also a transition in the composite system where that validator can take that transition it sounds it sounds kind of it sounds weird but basically the it's it's not the local condition lifts to a distributed one um and so basically um this local component is checking about a condition that's distributed across the whole composition and that's sort of um non non-trivial because of information uh disparity between the nodes so um there's um a message here being received and this is the message being sent and this is the label and this is a a constrained transition which doesn't necessarily mean that m is valid however it's lifted to a valid condition transition with M being received so so basically the validity condition of the component is enough to guarantee the validity of the message received in the composition so basically the component locally is able to verify whether the message has this distributed property and that's why it's called a validator because it's basically able to check something that's outside of its scope um and it's again defined here with respect to a particular composition and a particular con strained on that conversation so you might to have different validators for lots of different distributed settings but we're specifically going to be interested and focused on uh equivocation for um you know a reason that I've already talked about but like sort of like reveals at the end like uh why equivocation is so uh particularly interesting to look at so um this the the equivocation Theory section talk about evidence and then using evidence to describe compensation constraints that limit uh and validity conditions that limit equivocation and then we talk and then we'll talk about models of equivocation and then all this will tie in nicely um the in the when we start talking about bustine FS so this is sort of um what we're used to seeing in uh blockchains when it comes to slashing conditions um this is a a starting point um or was a starting point in in in our uh proof stake research um basically when messages have the same sender um they' they they've been they're like collected by the same node or like in the same smart contract you can imagine and and and they and they basically could not have possibly been produced by the by by this by the sender in a single round of the protocol so if you run a trace of these things there isn't a single trace where those two messages are produced by that note uh and so and and so this is evidence of equivocation this is somehow um we have two messages that couldn't have been produced by their sender uh and we have them sort of in the same state um this is sort of a sort of faulty behavior and this is local evidence and here's an interesting definition yeah yeah of course sorry um uh if we don't have a history how do we check that what uh yeah yes so it's it so that's a good question I mean it's it's I think it's undecidable in general but uh the question is whether it could not have been possibly produced by so basically you need to sort of quantify over all traces and say there is no Trace uh where these two messages can be produced so in practice you know we're going have lots of simplifying assumptions like you're indic like you're guessing you know um but the the definition doesn't say how you know how we can how we can come to this decision about whether a message could have been produced um you know it's okay we that's actually another nice thing about having the validity conditions as uh sort of like predicates you can have undefined sorry undecided um conditions whereas uh you know if you were using partial functions that would be an issue um so uh there there uh Global evidence is a little bit more interesting and a little bit more uh um maybe a little more decidable right because you in in this this we have like a sort of global view of uh of the of of of the trace so we can basically check uh that the message was not observed uh in in so um yeah so so so so so this is this is this is getting into some later content that I was hoping to I think I've slightly misordered this um but anyways uh if if you have if you have a if you have a God's eye view of a VSM uh trace and you re and you and you have a message that wasn't sent by a component but it but it was received by by some component um that's an equivocation sorry Denisa could you go ahead no mhm um yeah um so here's a uh theorem right that the the the the local equivocation is always going to be less than the global equivocation and all these are checked in the theorem provs but you can sort of imagine why why that is um and basically we can use these Global and local definitions of equivocations to limit the uh equivocations to create basically a composition constraint where the Faults Are um are limited um we can easily just say okay well there shouldn't be any equivocation and and talk about DSM traces where there aren't any equivocations um and we also use the full mode assumption um to reduce the amount of equivocations because then you can only sort of get an equivocation from the sender of a message because you've already received all of its dependencies um we can limit equivocations um to just a subset and we can also assign weights to the nodes and then limit the equivocations by their total weight um these are like example conditions in composition constraints um or a local constraint so this is a composition constraint for a validator on on on a global constraint that looks like this um and so like in this particular example this validator is just checking the local equivocation weight and if it's less than T when the and the composition constraint is checking the global equivocation and the the validator property is basically that from the local one there should be a global a state where the global one is also satisfied um basically the lifting property of the valid state from the uh local to the distributed property so you know this was talking about basically what what what equivocation looks like and how to detect it and therefore how to talk about you know non-c constructively traces that have uh limited equivocation um but we do have a a very nice constructive sort of uh approach to where we can describe uh equivocator and um basically there's two models for equivocation there's a state equivocator which basically splits its current state up or has many Poss many states uh for the same validator um and it can do that by forking or by starting new machines um and it also has and there's also the message equivocation model where instead of the state splitting and having multiple copies of a validator um validators can receive messages that haven't been sent um and and sort of this this sort of um uh is is is what is is is what we're observing um in that Global in that definition of global equivocation um and and it turns out that these two things are equivalent actually um the traces that you can get from the equ state equivocations and the message equivocations are the same uh whether you are like receiving messages that haven't been sent or splitting up States uh if you like project down to those equivocator States we get uh exactly the same traces um and it's kind of it's kind of interesting basically like splitting a timeline and communicating across timelines um uh end up producing uh exactly the same States and so these two are um models of the same uh phenomenon um equivocation and that's why we have those two definitions there where one of them seems uh a little bit different than the other um um you know somehow uh two messages that couldn't have been produced in a single trace evokes a state equivocation and uh a message that hasn't been sent yet being received evokes the message cation but um they are uh they are equivalent um so that's um a pretty cool pretty pretty pretty cool result that's going to be useful later um but basically to repeat it um the models of equivocation that um where that split the state and models equivocation that allow communication from other traces uh lead to the same traces for uh validators um for a limited equivocation so um that means that when you have um evidence of equivocation being produced um you know you can produce that equ uh that evidence either with State equivocation or message equivocation and get exactly the same state exactly the same uh evidence great so that's first two sections any any questions before the next one excuse me so here we go yeah please your microphone's off sorry you try okay I guess in in the previous discussion you kind of assumed finite branching which means that you cannot make infinitely many copies at the same time no we have we have unbounded we have like a list like unbounded list of copies okay but still finite right yeah finite but finite unbounded yeah yeah yeah because when it comes to infinite messages and states I was like um yeah um um that's a that's a good question I think we have possibly infinite uh traces but not States and messages the moment yeah I guess so sorry about that we we'll get we'll get there um yeah so so so so now basically we're going to do yeah go ahead yeah please use my microphone microphone just close just hold it closer oh no never mind sorry hi can you hear me yeah that's great this is great sorry um I think the States can be infinite but not reachable it's a matter of which are the reachable states but the it matters how many labels you have and that gives you how many moves you can do but in reality yes it's bounded and yeah great so let's move to the business uh the Byzantine faults so um basically we can model Byzantine faults in VSM by uh replacing a node with a a node that basically has a free behavior that uses labels to send uh and receive any message at any time um the important behavior is that it can send any message at any time um basically uh modeling U someone that can send uh you know any sort of malformed in uh invalid message at any point um and and we do have a little bit of constraints which is that we we don't let them Forge messages on other nodes and uh we do have a full node assumption um but um uh you know they can send any message you know signed by them um from from from them basically without Forge messages inside um and so we can replace equivocation uh limited validators uh with bantine components and find that they have exactly the same traces um the ones that aren't replaced have the same traces um so the if you have a trace in the equivocation limited uh composition where like some set B of of validators is uh Byzantine um they have a the same traces um uh as if they're composed with equivocator instead um and basically that's because of the validator property so if you have a validator property um on a receiving a message from a Byzantine Center that means that there is a composite state where um that sender as an equivocator um can validly send that message um because here we're validating for a limited equivocation setting so you know some amount of equivocation is valid in that setting um and so we can replace this these Byzantine nodes with uh equivocating nodes and then look at the traces of the of the valid D that aren't equivocating and show that they have exactly the same uh traces um um Dena do you have a question okay um and the same result also holds for uh uh weight limited equivocation model um so it's not just a for fix set but for under t- limited equivocation weight um all the behaviors uh that of of non-e equivocating components uh due to equivocating components is uh exactly replicated uh by uh bantine Behavior Uh with the same t uh uh limit um and so that basically means that Under The Limited less than T weight equivocation we get all of the same traces for the validators as limited less than T weight business vaults um so that's sort of uh the uh sort sort of magical way that we can not use Byzantine fall tolerance um basically for these equivocation limited validators equivocation Falls are exactly as expressed as binee faults because by validating for that limited faulty setting um uh you know they're uh restricting their transitions a lot and if a Byzantine Byzantine node can sends a malform message that they receive that means that that transition can be lifted to a valid state in the composition Under The Limited T equivocation condition um which means that there are nodes in the composition distributed that ify that less than T threshold um but uh um you know AR aren't bantine notes but equivocation notes and then um you know do like putting those transitions together to get traces we can rebuild exactly the same traces um and so basically this forms an alternative to for analyzing faulty distribut systems to Byzantine fault tolerance and quite uh um simply you know um um by studying uh equivocation limiting instead of and equivocation f faults instead of uh Byzantine faults so somehow equivocation Faults Are like a special kind of fault where if you validate for limitating equivocation that's just as good as validating for um limited business tee faults oh sorry that's just that's just as good as um sorry that actually lets you throw out bantine fault tolerance analysis alt together when just when thinking about like what traces you could go to um you can sort of just go to the protocol defined ones and um um it doesn't really matter what the uh Byzantine nodes do they're basically just protocol following equivocator as far as uh the analyst is concerned and so instead of having misbehaving nodes they just have either like you know a state replicator or message uh passer that sort of uh crosses timelines um which is sort of much more tamed types and well- defined uh Behavior so later we're going to relax the full note assumption and treat synchronization faults I'm out of time thank you so much uh thanks for coming really appreciate it if you have any questions you can find me outside later thank you