Formal verification has long been the gold standard for uncovering subtle bugs in distributed system design [1]. While AI has already proven its ability to accelerate verification processes [2], recent breakthroughs suggest a far more transformative potential: AI can now autonomously generate accurate formal specifications directly from very large production codebases. This capability marks a pivotal moment in software engineering, pointing toward a future where AI-driven correctness verifica...| Cheng Huang’s corner