Do you know any language/system which builds around invariants and the change of invariants in the evolution of the software? To me Prolog feels somewhat like that with its "relation" like facts/rules - which can be more and more refined.

What kind of invariants? In general, any strong type system is practicing a limiting of the search space by some kind of invariant. Haskell libs in particular can derive code/functions from specified invariants while dependently typed programs like Idris conversationally limits/builds types and code.

it sounds suspiciously like this isabelle proof assistant talk I saw over the weekend, invariants and refinement:

Yeah guys, I think the very best answer to that is what you have answered: "what kind of invariants" / Dependent Types / Proof Assistants. :) I was afraid of that because those are my answers as well! :) I asked the question because half part of my intuition says there must be some useful system I am not aware of on the level of logic programming where Prolog sits, but the other half of my intuition accepts that the most sophisticated way might be the Dependent Typed / Proof Assistant way to go on.

I believe CQL also has an approach to this kind of thing: they generate adjunctions for schema changes given some constraints and relationships

Ty, I’ll look it up!