I don't fully understand what you're objecting to. Are you saying it's not possible to build a formally verified container orchestration thing?

I do think that most software out there is unsafe. That doesn't make it useless, but if the effort required to exploit vulnerabilities is decreasing we will probably need to stop building things that way.