Yes, but the implementation is very different. These model checkers aren't turing complete, and because of that they can give some strong guarantees about what

Yes, but the implementation is very different. These model checkers aren't turing complete, and because of that they can give some strong guarantees about what they can and cannot do. Prolog? Shift some things around and watch your program suddenly run forever or so slowly as to be useless. If you want to mess around with something very prolog like but using similar kinds of underlying tech to these model checkers, try playing around with ASP solvers like Clingo/Clasp or DLV