I've not looked at ZZ yet, but when we talk about formal proofs, we're usually proving much more interesting properties than what a type system typically proves.