# Deep Dive into Fork Choice Compliance for Ethereum Clients | Devcon SEA

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2025-10-09
- Duration: 23:44
- Topics: Science & Technology
- Watch: https://streameth.org/watch/yt-N5WzD8ptGJA
- YouTube: https://www.youtube.com/watch?v=N5WzD8ptGJA

## Description

In this talk we will share the design of the methodology checking the compliance of Ethereum consensus layer clients to the fork choice specification. The core of the methodology is based on the constraint solver models which allows to generate huge number of distinct test scenarios providing comprehensive coverage. At the current stage we have ended up at around 13,000 fork choice tests, but the test suite we developed allows to generate a million of tests and even more.

Speaker(s): Mikhail Kalinin, Alex Vlasov
Skill level: Intermediate
Track: Security
Keywords: Core Protocol, Fuzzing, Testing

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] wow a lot of fans in the audience yeah hello everybody hi everybody yeah today we'll talk about uh FK Choice compliance and how we approached it and to start let's understand uh first why FK Choice compliance is important uh the FK Choice rule is the part of etherum protocols that that decides on the head of the canonical chain uh that is the chain that is the chain that you use to confirm your transactions that is the chain that will be eventually finalized uh by the protocol and uh a noncompliant with the FTR speack implementation can cause uh different security issues such as confirming your transaction with the chain that your local node pretends to to say that this chain is canonical but the chain is effectively not canonical and it's not canonical to the observation of uh the majority notes in the network um in some situations uh this uh non-compliant implementation can cause uh Network splits uh which can affect validator voting uh participate valer voting rate uh in a bad way and uh in the worst case scenario it could delay finality um in Ideal World uh every every implement mentation is formally verified to be compliant with the for CH spec but we cannot expect this to happen because it is quite challenging and costly and our approach to the compliance is to extensively test every implementation against the FK Choice spec uh so now a bit uh about the folk Choice rule itself so imagine there is a node state that is computed from the messages that are coming from the network such as blogs votes and others and the folk Choice rule algorithm is executed over this state in in the following three steps so at the first step there is a filtering function that uh selects blocks that are candidate for head we call them viable for head blocks at the Second Step uh validator votes are used to compute uh weights of sub trees uh which contains those uh wable blocks and uh at the last step uh the algorithm recursively goes uh down to the heaviest sub tree until the leaf block is found and that Lea block uh will be the head so the algorithm doesn't look uh um quite doesn't look complex it's Rel relatively simple but uh the complexities here uh coming from the different place uh there are many many inter notd interacting in the network and they produce many messages blocks and votes uh that results in a huge variety of States over which the folk Choice algorithm is evaluated and every client implementations use uses their own optimization in order to compute the state fast and uh in order to uh run the FTR rule so those makes those two things makes the the F compliance incredibly complicated uh and now over to Alex on how do we fight those complexities uh so our goal is to reveal difference between Fork Choice specification and implementations and we need a lot of interesting test scenarios but generating lots of really interesting scenarios is a challenging problem and so to overcome that we developed a strategy which based on the following principle differential testing property based testing modelbased testing and final ingredient fing and randomization and okay about differential property testing for Choice spec is executable so we can compare implementation Behavior against specification directly and this is why differential testing and we want to check that uh every implementation calculates the head of canonical chain correctly but it does not mean that so if the check the head is correct it does not mean that protocol state is correct too and so we can check additional properties uh to reveal more buxs with using essentially the same test seed and uh here is the example of how the property checks can be really helpful uh on the left side there is a buy implementation that for some reason just missed one vote uh and uh the head in in both cases in case of implementation and specification is the Block C so this V this Miss vote Miss did not affect uh the had computation uh and if the test case would just compare the head uh and uh the the client this bu implementation uh running this test case uh would pass it successfully and uh directly comparing the weight of Block C in this case uh would help us to reveal bug much easier because otherwise we would need to create a test that uh in which run in which this bug implementation would would lead us to uh the different uh block to be the head like for instance Block B so is just uh like less test can can reveal more boxs that's uh the short uh description so uh yeah what we haven't yet mentioned is that our compliance uh Tool uh leverages on the already existing folk Choice testing framework uh there is the consensus in the consensus specs there is the fork Choice testing uh format there are manually written uh Fork Choice tests and clients already run them those are integrated uh and yeah the the clients already uh check some of the properties so the differential property based testing is already in place and what we we do with uh our in our compliance tool is just add one more property uh which uh is to check weights of viable for hat blocks okay so we want to check that for Choice uh Ro is executed correctly but just covering various execution pass is not enough because um the through executed on many nodes and they're interacting and building blocks using the rule and so we actually what we want is to capture this interactions but we do not uh enumerate all possible scenarios and so we use modelbased approach um our models basically allows us to focus on the aspects that are interesting abstract away from other stuff and we have three models here FFG checkpoint three shapes block three shapes and also filter block three predicates coverage model and each models for example we have 10 blocks and we have various trees constructed of of these 10 blocks and so we basically want to generate a test Vector for each of these three shape and if we are able to to do that then we have 100% coverage of our model and for our three models we currently uh optained a thousand of solutions but in practice it can be arbitrarily larger so it can be a million models no problem yeah so to give you like more intuition behind how this uh model based generation Works let's consider the F ofg check points model uh this model is parameterized by two main parameters uh which are uh of EPO and number of Super majority links and here is the example of a couple of solutions that satisfy uh this model with four EPO and two super majority links and uh on the on the if you look at the top uh deok number four uh in this case will be finalized according to FFG checkpoint to to to to the finality Gadget rules and uh in the SEC in the in the second case which is on the bottom the e book number two will be finalized so basically uh when we do the test generation we ask the constraint solver to find all possible uh combinations of Justified and finalized points given the um some certain model inputs and uh we also run uh this these models uh with uh different inputs like uh you can run it like with 10 EPO and five Super majority links with 10 ooks and four super majority links and so on and this is gives us a lot of uh a lot of uh solutions to further work with uh in our generation okay so now we have uh many model Solutions and everyone can be turned into a test Vector but that can be done in different ways for example validators can vote for different blocks but as a result we can have the same shape and and so we use randomization to instantiate these model Solutions basically flipping a coin and uh after we have a test Suite of test vectors we can additionally do fing um it's important because our models actually assume that all events arrive in time which is unrealistically but we can easily overcome it by shuffling uh duplication of messages and dropping some messages and also by mutating messages we will also plan to implement in future coverage guided fing of implementations and this uh randomized instantiation and fing allows us to increase the number of tests in by orders of magnitude yeah here is the example of how the randomization is used uh as Alex mentioned we have these model Solutions and we use them to uh produce uh like various test vectors and on the top there is just a model uh which which says that basically there is a block that has two children the client has nothing to do with this model it cannot run uh this model because uh to to to make it a real test Vector to make it we have to make it a real blockchain that follows the ethereum protocol rules and uh we use consensus spec uh specs for for doing this for making a these blocks turn into uh making this uh block dependency to turn it into real blocks and real votes and in this case the model does not answer you to many many questions that the protocol need to you know to to to create an instance of a blockchain those questions such as like uh which validators are voting for which block every single slot uh where where is the maybe there is an empty slot between those blocks uh which is the total number of validators participating at Moment In Time whether the message is like some message is invalid or not and so forth and for every case for every possible case here uh to answer such questions to to decide on such uh things we flip a coin so we have like a every every test generator run there is a combination of model solutions that we use and a randomness seed and uh running the same uh combination of model Solutions with different Randomness seed can yield a different uh test Vector what matters here is that this test Vector will be completely different uh from the FK Choice point of view so like in this uh example there are the had TS a different so but the model is the same so we have implemented the initial phase of the strategy and this work was supported by a grant from eum foundation and but from consensus and so we have a test generator we have a PR in consensus spec repository we have generated three test Suites to Tiny and small uh the test Suites for initial adoption and we also the main standard test Suite which contains about 13,000 of test which I believe is enough for initial phase yeah and so we did the as a prototype we did the integration of this tool in taku as I mentioned before uh there there is already uh the F choice test and clients already know how to run them so this integration was relatively straightforward we added the new property check that mentioned before uh found some issues a couple of them are related to optimizations I'll cover this uh on the next slide and we found four Edge case uh four edge cases uh where where TECO is not kind of like compliant to the spec but these edge cases are very very unlikely to happen on any any test net uh including the main net and uh uh the fact that we found those edge cases uh shows us how powerful this tool is with only 13,000 tests just imagine what would it be like uh if we have like a thousand uh 100 100,000 tests or a million tests and we're looking forward to have this tool in to have this uh suit integrated with other uh consens layer clients to find issues in them as well so let's look at test Suite details so we have uh test groups inside test suits for example block three focuses on trees of various shapes and block weight we try to produce block trees where weights are different distant from each other we also have a shuffling group and uh test group which focus on a test s invalid messages and combinations of filter B three predicates and overall we have about 13,000 of tests right now okay uh so we have problems and one pro uh problems is that advanced mutation are challenging to implement for example if you change a block we need to rec compul recalculate its cash and descendant blocks and attestations should be recalculated too and this uh takes time so test generation is slow currently it takes about 10 seconds per second we have investigated the reasons for that and okay one reason is that fork Choice Ru is expressed using python which is an interpreted language and it's low we but that's not the only source of the problem because there are also some slow spec components they are optimized actually but there are still a room for improvement and this uh slow test generation limits uh the Practical size which we can achieve yeah as I mentioned before there are some optimizations that uh cause some test fail uh and those optimizations are that we have faced with are related to uh dos protection so some AR stations some old attestations that are not going to affect the uh folk Choice decision are discarded in Teo for instance and in other clients as well and different clients use different her istics to discard such attestations and here we have another problem uh is that the uh the two the the cute cannot be designed to uh to avoid all those uh failures and uh diff and because of different clients has different optimizations and different her ristics there will be different subset of tests that are failing and uh we have like just 13,000 tests but imagine if we have a million tests and you have like uh I don't know thousand of tests failing and you have to ensure that you have to real you have to understand whether those are uh because of such optimizations and this is legit case or whe this is a real bug so this is something to work with the client developers on and as a Next Step as a next low step we want to integrate this test you into other consens clients here we engage other client developers to to help us with and yeah yeah okay so one of the most important things to do is to speed up test generation and okay one thing that we want to do is to transpile specification to C or to n rust other compiled language and of course there a problem that a transpired code there can be a bu into the translation but uh since we are translating function to function it's actually much easier to test each function individually individually and another approach uh another important thing is that to optimize all components we have already experimented with faster implementation so we as a result we expect uh that our test should run uh test should be generated at least 10 times faster and also an important thing is to implement coverage guided fast testing of client implementation and for this reason we it's critical to have fast test Generation Um so if you want to talk about this topic reaches out you can also find us on E andd Discord here is the core code which uh links you to a page uh with the references uh to the work we did there is a description of the test and methodology there is a uh link to the pr to this pack which introduces the test generator for this suit and also there is the pr uh that uh PR to te that integrates the Su into Teo thank you very much thank you thank you very much Alex and mik all right great to see you got a lot of support from the audience that's fantastic now I wish I could say I understood the topic of the content but I didn't but I'm sure the audience because they're asking lots of questions I'm very honest about it you know uh please upvote your questions which are most popular and we're going to look at the screen and take a run through the questions right at the top do you run Fork Choice tests covering nonf finalization with multiple Forks who'd like to take this question I I love this question because I before this talk an hour before this talk I was thinking about having this test in suit because if you have if you've been at the dep Lance presentation who was presenting on the non-f finality and how can it kill ethereum this is very important for clients to have this kind of testing suit uh we haven't think thought about this much but I think it is doable uh and yeah I'm I'm very happy to discuss this um and try to make something uh and try to make a suit that would test nonf finality and let clients do their optimizations and uh check them by just running this on the computer excellent from one one question can change everything right uh now the question at the top this test generator Rock so another round of applause for creating such a wonderful test generator again if you want to give feedback before you go into the Q&A there's a little box for speaker feedback please go and write it there so the speakers can take take a look at that but well done to both of you let's go to the next few questions do you plan to set up a dashboard to show test results from different CL clients like Hive who wouldd like to take this um I'll take this I we don't have such dashboard for other CL tests we have a plenty of Cl tests that are uh run by clients and yeah I haven't thought thought about it we haven't thought about it so probably not because yeah if it will be useful we can but maybe not okay all right let's go straight to the next one what does it mean for the fork Choice spec to be executable go ahead yeah I'll take one okay so um it's expressed as a python code so it's basically a number of functions and some functions prescribe how to react to events or messages arriving from Network it's on block on attestation on on a tester session and some others there's also time tick and finally you have a method to get head so this is just by PL python code you can run it all right let's go right to the next one we got three questions left I think we got enough time the randomizing weights model can take an arbitrary tree as model question mark how about FFG information who would like to answer this one I can yeah so uh the Tre block tree model is just one of the models uh and there was just an example so with randomization and uh we also have the F ofg checkpoints model that gives the all all possible uh combinations of Justified and finalized checkpoints given the model input so it was in the presentation as well so we have a model for that it is also this information also used by the test generator all right thank you for answering that I'm going to mark it as answered last two are attestations only on chain coming from blocks uh no no uh we have both cases so we have uh get a two station from blocks also produce them separately very um I can expand on this we have actually have three uh possible cases for this one is that just in pure onchain attestation the other one is uh pure Network attestation that the attestation that is not included in any Block in any block and the third case is both it is in the block it is on chain and it is coming from the network as well and this is all decided by the randomization so we flip a coin and decide which station uh would will be in which state all right thank you for answering that you're looking at me like I understand the answer I don't but the audience I can tell from the audience is nodding and I'm just nodding along with them U okay we got uh one vter okay we got 51 seconds let's do it if the model is written to test the spec implementation how do you guarantee the model correctness okay the model uh does not have to be correct because we execute python specs directly so we use it just to produce interest in test vectors and yeah we are using spec code to produce the text vectors but finally we have a special procedure to run the generated test using um the python spec and check the everything is okay very good and I believe I can help you answer do you execute the python spec directly yes you do ladies and Gentlemen let's give our two speakers a wonderful Round of Applause to Alex and mik thank thank you gentlemen thank you thank you very much