TLA+ and Alloy are lower barrier to entry software verification tools. They are typically used on systems or protocol level models rather than modelling the exact source. There are many bugs that can appear at this level and they are super useful for clarifying your thinking.
