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).
I also wanted some wiggle room for languages that are fairly researchy but some people do use them in real life for hosting blogs and such, like Idris.
There might be a few others. https://github.com/google/wuffs for example isn't general purpose or mainstream, but it's meant to solve practical problems, so I don't think I'd call it a research language. Opinions may vary.
