Agreed on lightweight formal methods. TLA+ and Alloy have been really eye opening to use, and it's almost at no cost. They're just tools for expressing logic and analyzing models.
Even those are very heavyweight to my mind. I’m thinking things as simple as applying semantics to flow charts and making state tables. Exhaustive enumeration of small spaces forms a neat on-ramp to more powerful methods, if we choose to treat them that way.
