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 It is also available from Maven Central (https://search.maven.org/#search%7Cga%7C1%7Ca%3A%22de.prob2.kernel%22)
- Website: http://www.event-b.org/
- Handbook: https://www3.hhu.de/stups/handbook/rodin/current/html/
- A very approachable book is https://www.amazon.de/B-Method-Cornerstones-Computing-Steve-Schneider/dp/033379284X/ref=sr_1_fkmr0_1?ie=UTF8&qid=1533383324&sr=8-1-fkmr0&keywords=Steve+Schneider+B-Method
- A Book on Event-B: https://www.amazon.de/Modeling-Event-B-System-Software-Engineering/dp/0521895561/ref=sr_1_3?s=books-intl-de&ie=UTF8&qid=1533383359&sr=1-3&keywords=Abrial