I feel like it's much harder to shoehorn in proofs to existing codebases than it is to start with the proofs first.
The automation in Isabelle is quite good; good enough to where I don't feel that writing pure new code with proofs takes me a prohibitively long amount of time (about 2-3x writing the equivalent Haskell) (sledgehammer ftw), but I can't imagine trying to retroactively go and prove any of my old projects that are considerably smaller than 20 million lines.
One big perk for using Isabelle (or other proof systems), outside of the obvious correctness proofs, is being able to prove equivalence. If you can inductively show that two functions have the same inputs and outputs (say one was quick to write or easy to prove things about, the other is efficient), then you can tell the code exporter to replace any instances of the inefficient version with the efficient version. This means that your optimization is proven safe, and is done for free, which is worth its weight in gold when used correctly.
Of course, this really only applies to pure and mathey functions. It's substantially harder to prove properties about business logic.