Types are the world's most popular verification technique. The whole intent of types is to automate many of the proofs required to guarantee the correctness of

Types are the world's most popular verification technique. The whole intent of types is to automate many of the proofs required to guarantee the correctness of the program rather than having the human operator get bogged down in verifying the details themselves. Now yes, you can't verify all aspects of the program but types can still get you quite a distance of the way there at comparatively very little cost compared to more heavy formal verification techniques.