Hi, I'm one of the main devs. TLA+ is useful to prove properties of programs. By contrast, IDP-Z3 is a reasoning engine that can be used as a module in a program. It is closer to a constraint solver, but offers more functionality than a traditional CSP solver. For example, it can compute what are relevant questions, given some inputs. This is useful to build "interactive consultants".

For example, you give IDP-Z3 the formula that links a tax-free amount, a tax rate and a tax-included amount, and the values of any two of its parameters, and it will compute the missing parameter. You do not need to write 3 different formula, one for each case. If you give him only one parameter, it will say that the other two parameters are relevant.