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."
replyYeah, 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
replyIf you're excited about the relationship of Lean4 to LLMs/AI (like I am), you might find my recent post interesting [1].
replyTL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.