>But they where harder to implement and very complex

This is the general trade off for being correct. Being mostly right is easy, but leads to complex security issues later. Being correct is very hard, but should reduce the number of flaws to a manageable level.

I think Lean or Ada would be examples of different types of correctness contracts.