Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are ver

Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are very intertwined; it's not really possible to build a proving system in this metatheory without also allowing for program verification. Maybe you're talking about gaining support for formal verification of code not written in Lean? Like, being able to verify C? In that case, it's actually just a library issue. Nothing needs to be changed about the core Lean language, someone just needs to formalize the semantics of the target language semantics in Lean, and then add a verified compiler and verified extraction if you want to make the guarantees extend directly to the compiled assembly. Fuzzers have actually combined well with theorem proving in these kinds of tools in the past; Coq, the proof assistant that heavily inspired Lean and has been in constant use since the mid 80's, has a library QuickChick (based on QuickCheck from the Haskell world) which takes an arbitrary property and generates test inputs to test it, and has very mature support for extending it with new datatypes and invariants.