An online textbook covering standard topics in undergraduate algorithms. Every algorithm is written in Dafny, a language with built-in support for formal verification. The emphasis is on loop invariants: understanding why an algorithm is correct, not just how it works.