PREDICTION: AI WILL MAKE FORMAL VERIFICATION GO MAINSTREAM

Summary from the TLDR InfoSec newsletter

Formal verification is a highly specialized and time-consuming process of mathematically validating a system's behavior. The 8,700-line seL4 microkernel required 20 person-years and 200,000 lines of code in the Isabelle proof language, underscoring why formal verification remains largely an academic discipline at present. If we instead train users to write proper specifications for formal verification, it may be possible to use LLMs to generate proofs and reduce the barrier to formal verification.