01
Dafny: Writing Programs and Proof Obligations in One Language
Rustan Leino’s Dafny made specifications, executable code and automated verification part of one programming language, using Boogie and SMT solving to check functional correctness as developers write programs.
↗