If this algorithm is used to dispense some type of medication, and I enter 3.1 and it murders you with 10 grams of alprazolam... well.... the algorithm is still correct.
Nobody is saying the formal proof approach will find all bugs, just that it helps find more bugs compared to not using it. You could make the same argument with acceptance testing: unless you specifically tried 3.1 as the input during testing, it might not give you the output you expect. Formal proof can be complimentary to traditional automated tests and QA.
For any non-trivial code, no matter how much formal analysis you do, you don't trust it until it's been properly tested.
How many intricately specified software projects have failed because the spec bore no correlation to user needs?