This is the web site for the early stages of a book introducing both machine-checked proof with the Rocq proof assistant and approaches to formal reasoning about program correctness.
6.512 at MIT (Fall 2025, Spring 2023 [as 6.822], Spring 2021 [as 6.822], Spring 2020 [as 6.822], Spring 2018 [as 6.822], Spring 2017 [as 6.887], Spring 2016 [as 6.887])