If you're interested in playing around with loop invariants for non-trivial programs, I recommend the Dafny programming language which can automatically verify

If you're interested in playing around with loop invariants for non-trivial programs, I recommend the Dafny programming language which can automatically verify the invariants using SMT solvers. (Dafny is much more convenient that messing around with operational semantics in Coq.) There's a tutorial + web interface at: https://rise4fun.com/Dafny/tutorial/Guide https://rise4fun.com/Dafny/tutorial/Guide. The official repository is here: https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny -- you might want to switch to a local installation once the online tutorial whets your appetite. A good initial challenge, once you've gotten past the baby stuff in the tutorial, is implementing insertion and deletion on a binary search tree with appropriate pre- and post-conditions.