If it's Turing Complete you can't prove that it's hermetic. You can't even prove if it'll ever finish running (halting problem).

Maybe someday someone will invent a sort of EBPF for containers, but usually the first batch of RUN commands and the last are calling package managers, and in between you're doing things like creating users and setting permissions using common unix shell commands, which have the same problems.

With the possible exception of the unix package managers, we have no hope of those ever being rewritten inside of a proof system, because the package manager is often a form of dogfooding for the language community. The Node package manager is going to be written in Node and use common networking and archive libraries. Same for Ruby, Rust, you name it.

> If it's Turing Complete you can't prove that it's hermetic

Turing Machine model doesn’t apply to i/o so it is a meaningless statement.

Bazel and Nix achieve this by sandboxing i/o no turing incompleteness needed (tho bazel is still purposely non-tc but for totally different reason than hermeticity)