Well if you go for proof of absence of runtime errors, it's SPARK, which is a (compatible) subset of Ada, and comes with a toolset to perform verification. Proof of absence of array-bounds errors or any runtime error (well except for OOM and stack-overflow - for now).

I'd add that Frama-C does also this kind of proof and IIRC Eve (Eiffel Verification Environment ?) too, though I find the SPARK workflow far easier and advanced (but we use it more so... I'm biased).