“Why use K as opposed to Coq?” Three blog posts using a working example to highlight important ways in which K and Coq differ as formal verification frameworks for languages: Part 1 , Part 2 , Part 3 .