Formal Verification Is Not Verifiable: Bouba and Kiki Software (alperenkeles.com)

Recent developments in formal verification have highlighted both its growing significance and inherent challenges within the AI/ML community. The surge in formal verification startups and projects, including notable partnerships like Theorem’s work with Anthropic, signals that formal verification is becoming a critical component of software development, especially amid rising cybersecurity threats. The shift in focus from "how can we prove X?" to "what can we prove about X?" underscores the increased economic value and practical application of formal verification methodologies. However, despite these advancements, the author warns that formal verification may not be as reliable as often stated. While AI has accelerated the production of formally verified software, the intricacies involved in verifying systems—especially those described as "bouba," or complex software—that incorporate user experience and visual design elements complicate the notion of correctness. Moving forward, it is essential to refine the language around formal verification, emphasizing what properties can be verified and the contexts in which they apply. The author remains optimistic about the potential of proving properties of single-threaded applications and suggests that integrating random testing and exploration could enhance validation efforts, fostering greater trust in formally verified claims.