This is same idea with onion architect in "Grokking Simplicity: Taming Complex Software with Functional Thinking Book by Eric Normand"

Interestingly, Huly is also the sponsor of the Zig programming language[1].

[1]: https://ziglang.org/

They are working on the next generation of Hulu in Zig. However, no final decision has been made since they are also sponsoring V (https://vlang.io) and Odin (https://odin-lang.org) :)

It seems it has a lot in common with Lamport's TLA+, can someone compare?

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.

So it's layer on top of the z3-solver right? That's a way to see it?

Yes. It uses a more convenient language than SMT-Lib to express "knowledge", and offers more functionality.