A Formal Model in K of the Beacon Chain

less than 1 minute read


I posted an article celebrating the successful completion of the first milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have completed the executable formal model of Beacon Chain in the K Framework.

Read the article here (also on Medium).