Model Checker for (a subset of) classical B based on Z3
Development releases are available from here.