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."
https://vitalik.eth.limo/general/2026/05/18/fv.html