Sure there's evidence of that. Maybe not in the move-fast break things social/mobile/local web world, but in the mission/safety/life-critical and real-time systems engineering world there is. Just takes a quick google search, for example:

http://electronicdesign.com/dev-tools/11-myths-about-ada

"As one example of Ada in an undergraduate setting, students at Vermont Technical College in the U.S. used the SPARK language (a formally analyzable subset of Ada) to develop the software for a CubeSat satellite that recently completed a successful two-year orbital mission. SPARK was chosen because of its reliability benefits. The students had no previous experience in Ada, SPARK, or formal methods, but were able to quickly come up to speed.

Of the twelve CubeSats from academic institutions that were included in the launch, the one from Vermont Tech was the only one that completed its mission. Many of the others met their doom because of software errors. The Vermont Tech group credits its success to the SPARK approach, which, for example, allowed them to formally demonstrate the absence of run-time errors."

I've read similar success stories for Lisp and Haskell. Rust will likely add more evidence as it becomes more widely used. Agda and Idris are also capable in this respect.

The problem is too many engineers are just day-jobbers, who want to crank out LOC and quickly add features that get them paid, regardless how sloppy their work or the tools they use may be, or how much work/cost it adds to the maintenance overhead down the road. That work can either be done up front writing bug-free code, or later during maintenance putting out fires, but it can't be avoided. Programmers who chose the former use the excuse "bug-free code is impossible so we don't have to try" to justify pushing the work off on the maintenance team later. But it's demonstrably false.

You can write a formally verified, simple Hello World program and prove that it adheres to both your design and implementation specifications. You can this all the way down to how the specific processor will run the resulting machine code.

The catch is that this is difficult and the time and cost both scale non-linearly with the complexity of the software. But if you can do it for dead-simple programs running on hardware you understand very well, you can do it for complex software as well. Just be prepared to pay millions of dollars for it.

> But if you can do it for dead-simple programs running on hardware you understand very well, you can do it for complex software as well.

Not necessarily when you're bounded by reality and finite amounts of time and energy. Just because you can count to 2^8 doesn't mean you can count to 2^128.