I've wondered for a time how formal verification e.g with Lean might turn out production code. One way, used at AWS, is through differential testing. Prototype the software in the verification language, and then use the formally proved code as the prototype / spec for the production code. Next, run identical tests against the prototype and the production code. This at least proves that the production code behaves (within set variances) exactly like the proved-to-be-correct prototype does.