ProB can animate and Model Check (and many more) for B, Event-B, Z, CSP, TLA+
- Website: http://www.prob2.de
- Download (TCL/TK): https://www3.hhu.de/stups/prob/index.php/Download
- Java Version (will replace the TCL/TK Version): https://github.com/bendisposto/prob2-ui/blob/develop/README.md
- Online Logic Calculator (Constraints only, no Operations/Model Checking): http://wyvern.cs.uni-duesseldorf.de:8443/index.html
- Handbook: https://www3.hhu.de/stups/handbook/prob2/prob_tcltk.html
ProB can be used as a library in Java code to solve constraint problems, the library can be found under https://github.com/bendisposto/prob2