The only ones I've seen that delivered [with caveats] were Concurrent Pascal, Ada's Ravenscar, Eiffel's SCOOP, and recently Rust. SCOOP got the most CompSci work with a Java port, one proving no deadlocks, one proving no livelocks, a formal verification in Maude that caught problems, and one modification to almost entirely eliminate performance penalty.

So, it can happen but does rarely enough to arouse strong skepticism. I usually don't buy it.