This is really exciting.

I am an absolute beginner at TLA+ but I really like this possible design space.

I have an idea for a package manager that combines type system with this style of deterministic testing and state space exploration.

Imagine knowing that your invocation of

   package-manager install <tool name>

Will always work because file system and OS state are part of the deterministic model.

or an next gen Helm with type system and state space exploration is tested:

   kubectl apply <yaml>

will always work when it comes up because all configuration state space exploration has been tested thanks to types.