Specification Inference for Stainless Programs with Large Language Models

Sammanfattning

Writing formal specifications for program verification is a difficult and time-consuming task that requires knowledge of the verification tool and the program being verified. This thesis investigates whether Large Language Models can assist developers in this process for the Stainless verification framework, which verifies Scala programs using formal specifications written in Pure Scala, a restricted subset of Scala designed for formal verification. We evaluated three models: a locally hosted Meta Llama model, Microsoft 365 Copilot, and Anthropic Claude.We prompted them with 12 Scala benchmark functions, stripped of their existing specifications, and validated the generated output through Stainless. Llama, hosted on a standard home PC,only produced one specification that passed Stainless verification out of 12 functions, while Copilot and Claude performed significantly better, both with 9 functions passing verification. Both cloud-based models often produced specifications equal to or stronger than the specifications provided in the benchmark, though both struggled with complex functionsrequiring loop invariants or proof-level reasoning. These findings suggest that cloud-based LLMs show promise for assisting with formal specification generation, but are not yet reliable enough to replace manual effort for advanced verification tasks.