Vitalik recently wrote about vibe-coding in Lean and assembly language, using proof verification in Lean, saying "if done right, this has potential to both output extremely efficient code, and be far more secure than the way programming has been done before."
Yeah, his post resulted in a rise in everyone and their mother becoming formal verification "experts" now. But I think he's right. We no longer have good excuses for not trying to secure code with FV in this brave new world of agentic coding