Formal verification require a formal statement of what the software is supposed to do.

But if you have that, you have a recipe for doing property based testing: generate inputs that satisfy the conditions specified in this formal description, then verify that the behavior satisfies the specification also.

And then run for millions and millions of inputs.

Is it really going to be worth proving the program correct, when you could just run an endless series of tests? Especially if the verifier takes forever solving NP hard theorem proving problems at every check in. Use that compute time to just run the tests.