There are plugins for Haskell and dependently typed languages that go much further in the ‘if it compiles, it is formally validated’, but that’s a lot more work; there is a trade-off for now or you will be stuck. Your ‘run of the mill’ tests also don’t formally validate your logic (not even close usually). Our types, even if static, are usually too loose and our type systems not powerful enough; writing tests helps to close the gap between practical and theoretical but a lot more can be done semi-automatically (and will be I hope).