Tool for translating B to TLA+ for model checking with TLC. Alternative model checking backend for ProB.