You realise that definition also applies to hardware keys, right? They're unreadable, private data via memory safety - there's only limited interface to operate on that data in valid ways.
Proving code correct is far from obvious though. Apart from single instances like sel and python's sort, can you remember any verified software with proofs right now?
Memory safety is only a subset of verification. In fact, most programming languages are memory safe (although I think there are no formal proofs, I haven't come across memory unsafety in a language that claims to be memory safe).
seL4 is actually another verified software I know.
Proving code correct is far from obvious though. Apart from single instances like sel and python's sort, can you remember any verified software with proofs right now?