# Introduction to the Eth2 Phase 0 in Dafny Project

The following videos provide an introduction to this project, as well as more detailed discussions of several components including the state transition, fork choice and process operations.

### Part 1 - Introduction

https://user-images.githubusercontent.com/43776922/130721825-b9418cbd-10c2-4cd7-bf8b-7a36a67d0f4b.mp4

### Part 2 - Scope

https://user-images.githubusercontent.com/43776922/130721912-6c54e9b5-2fa8-420f-a52e-e5a037ec1961.mp4

### Part 3 - State transition (Part A)

https://user-images.githubusercontent.com/43776922/130722003-0e190dc4-7e93-409c-9ffa-f021809d4c44.mp4

### Part 3 - State transition (Part B)

https://user-images.githubusercontent.com/43776922/130722039-b57ce22c-10b2-4a6b-9d77-31eb9e21bdbb.mp4

### Part 4 - Forkchoice

https://user-images.githubusercontent.com/43776922/130722113-a2072216-fcdf-4dc4-aca0-3c56930adbfc.mp4

### Part 5 - Gasper-proof

https://user-images.githubusercontent.com/43776922/130722196-a8a4c5db-f927-4b71-8e43-40102a09d130.mp4

### Part 6 - Process operations (Part A)

https://user-images.githubusercontent.com/43776922/130722251-0e90c530-9fe3-4b43-a934-a830af90fdbd.mp4

### Part 6 - Process operations (Part B)

https://user-images.githubusercontent.com/43776922/130722300-ccae1ecb-a485-42a2-970a-c05c5c5a5c1a.mp4

### Part 7 - Maximum active validators

https://user-images.githubusercontent.com/43776922/130722344-732c0f64-7a07-4050-aebb-b1e10f65775a.mp4