The verification question is somewhat handwaved in the linked article, but in fact we are now in a position to verify some of this stuff mechanically. Unsurprisingly, the "branding" techniques work, but in type systems that have any amount of subtyping the argument for why they work is subtle and they may not work in all cases.