PI: Marie Whyatt

Formal verification is a well-understood method for proving the correctness of a critical system’s computer code at the highest rigor. It has long been used in aeronautics, medical, and military devices and systems, but until now, it has been a time-consuming manual process and thus is employed only in the most crucial devices and systems. Thus motivated, PNNL’s AI for Formal Methods (FM) project explored whether and how large language models could substantially reduce the time to deployment by comparing the ability of 12 large language models to correctly prepare computer code for formal verification, successfully moving the needs toward wider and faster adoption of formal verification in critical systems.