I mentioned Alloy a few times as a lightweight formal method. This has a really-short tutorial covering the verification of a queue and a map. They move from verifying static to dynamic aspects while comparing it to Z-based notation that came before it. Anyone casually interested in formal methods might enjoy how straight-forward their examples are with Alloy. It’s main advantages are ease of understanding, visualization tools for structures, and automation.