Indeed, ensuring that unsafe is isolated and obeys certain semantics is a superpower that few languages have rust+kani is a good and modern way to achieve this.

Oh absolutely. This is utterly unacceptable. The ease with which CS pushed willy nilly a bad build to prod in what seems to be a monophasic release is absurd.

Something of this nature would have had our entire team fired. The number of phases and the thoroughness and exhaustiveness of the protocols we have to ensure we don't push bad builds would have most engineers taken aback... but we have to. With great power comes great responsibility.