FizzBee is a totally new implementation of the model checker. It does not cross compile to TLA+. That said, FizzBee is also modeled after and totally inspired by TLA+.