Você pode verificar código com model checking sem aprender temporal logic
Bounded model checkers como Kani e relational model finders como Alloy permitem verificar propriedades com assertions e constraints ordinários. Você abre mão de provas de liveness por uma curva de aprendizado medida em horas, não em semanas.
