Comment by LtWorf

You don't seem to understand what I'm talking about.

bad axiom -> worthless theorem.

bad unsafe section -> verified safe section is actually not safe.