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.