How about the property 'this variable is never null'? You might call this trivial but it seems to be useful given that real-world programmers get it wrong frequently: http://stackoverflow.com/search?tab=newest&q=NullPointerExce...

Or the property 'this variable is never used after a free' in a language with manual memory management (Rust encodes this) or 'this program is free from data races' (also Rust)?

No one is arguing that strong static type systems make it impossible to write programs with bugs, but eliminating whole classes of bugs at compile time certainly makes it easier.