Yes, having used both TLA+ and Prolog extensively, they share many similarities (both having roots in first-order logic). In practice -- TLA+ code is often a bit more "imperative" owing to the fact that unbounded existential quantification isn't implemented in the TLC interpreter (whereas in Prolog, it is a core aspect of any interpreter).

And of course, TLA+ has a suite of temporal operators used exclusively for declaring contracts in service of its role for verifying specifications. Which (as @hwayne points out elsewhere) stem from mathematics -- Linear Temporal Logic specifically -- and not programming.

Eh, even though you prove things about your specs (possibly) there's still a difference between proof assistances and spec languages