Author: Daejun Park
![Formally Verifying Finality in Gasper: The Core of the Beacon Chain](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fethereum_logo_landscape_purple_d0e9145e6f.png&w=640&q=75)
![End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fethereum_logo_landscape_purple_d0e9145e6f.png&w=640&q=75)
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
by Daejun Park
January 20th, 2020![A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fethereum_logo_landscape_purple_d0e9145e6f.png&w=640&q=75)
A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain
by Musab Alturki
October 22nd, 2019Company
Resources
Connect
Mission and Vision|Presentations|Careers|News|Publications|Partnerships|Media Kit|Events