AI is transforming formal verification, making it more accessible and relevant. Companies focused on AI-assisted mechanical proving are seeing billion-dollar valuations, and interest in proof assistants, particularly Lean, is growing rapidly. This shift is evident in the performance of AI models in significant competitions and in addressing complex mathematical problems. Notable researchers, including Terry Tao and Martin Kleppman, are optimistic about the potential impact of AI on formal verification. The challenges in formal verification are primarily twofold. First, most software lacks a formal specification, which complicates verification. Without a clear mathematical description, determining what to verify becomes difficult. Second, proof engineering is inherently complex, varying widely across different domains. While tools for proof automation exist, they often struggle with reusability and brittleness. The rise of large language models (LLMs) in programming offers a potential solution by encouraging specification-driven development. LLMs can help create executable specifications, but testing alone is insufficient to guarantee bug-free software. Examples like the CompCert C Compiler demonstrate the power of formal verification in uncovering bugs that extensive testing might miss. However, the article raises concerns about the reliability of autoformalization. Since many programs lack formal specifications, relying on AI to create them introduces risks. The process of autoformalization, while beneficial, can lead to issues of soundness and completeness. Problems may arise when the formalized model misaligns with the verbal specification. Additionally, proof assistants often use inductive structures, which can slow down the verification process and overlook practical considerations like integer overflow. These limitations highlight the need for careful scrutiny of the tools and processes involved in AI-assisted formal verification.