I am thinking about state machine progressions and TLA+ style specifications which are invariants over a progression of variables. Your package manager knows y

I am thinking about state machine progressions and TLA+ style specifications which are invariants over a progression of variables. Your package manager knows your operating system's current state and the state space of all the control flow graph through the program and configuration together can go to, it can verify that everything lines up and there will be no error when executed a bit like a compiler but without causing the Halting problem. In TLA+ you can dump a state graph as a dot file, which I turn into a SVG and run with TLA+ graph visualiser. Types verify possible control flow is valid at every point. We just need to add types to the operating system and file system and represent state space for deterministic verification. You could hide packages that won't work. The package manager would have to lookup precached state spaces or download them as part of the verification process.