Try out Abstract, State Machines for math stuff. They've already had over a decade of research and field use. They were also rated easy to learn, like TLA+, for

Try out Abstract, State Machines for math stuff. They've already had over a decade of research and field use. They were also rated easy to learn, like TLA+, for programmers vs stuff like Coq or Isabelle. There's also tooling for them like Asmeta. Here's some links: http://www.di.unipi.it/~boerger/Papers/Methodology/BcsFacs07.pdf http://www.di.unipi.it/~boerger/Papers/Methodology/BcsFacs07... http://asmeta.sourceforge.net/ http://asmeta.sourceforge.net/ Also, type abstract state machines into search on https://lobste.rs https://lobste.rs for quite a few examples I put on there. We have lots of practical, formal, methods submissions plus some folks that do it professionally in there. Just click formalmethods tag.