Selene: Pioneering Automated Proof in Software Verification (2024)

Abstract: Ensuring correctness is a pivotal aspect of software engineering. Among the various strategies available, software verification offers a definitive assurance of correctness. Nevertheless, writing verification proofs is resource-intensive and manpower-consuming, and there is a great need to automate this process. We introduce Selene in this paper, which is the first project-level automated proof benchmark constructed based on the real-world industrial-level operating system microkernel, seL4. Selene provides a comprehensive framework for end-to-end proof generation and a lightweight verification environment. Our experimental results with advanced large language models (LLMs), such as GPT-3.5-turbo and GPT-4, highlight the capabilities of LLMs in the domain of automated proof generation. Additionally, our further proposed augmentations indicate that the challenges presented by Selene can be mitigated in future research endeavors.

## introduction confirming the correctness of the software, i.e., checking whether it adheres to the properties specified in the requirements, is advantageous for software engineering (se). in contrast to testing, which is incomplete, verification provides rigorous guarantee of software correctness or incorrectness @xcite . specifically, during testing, an adequate number of test cases are created and tested against the subject program. if the program violates a testing oracle or encounters other errors (e.g., runtime error), a bug is found. however, the opposite conclusion cannot be guaranteed otherwise. verification often involves the usage of a formal language and the corresponding prover. 1 this process requires formal proofs to rigorously demonstrate that the program satisfies the required properties, which can be verified by the prover. in general, software verification involves two stages. ❶ the prerequisite specification stage translates the required properties and the subject program into the formal language, creating a to-beproved proposition stating that "the program meets the properties", a.k.a., the specification. ❷ the proof stage is supposed to generate proofs that prove the above specification and can be formally checked by the prover. both stages consume significant resources and manpower, with the second stage being particularly demanding. e.g., the sel4 operating system microkernel foot_1 , which has been formally verified against strong functionality and security properties, requires 7 person-months dedicated to the specification stage and 11 person-years to the proof stage for correctness verification, and the amount of proof code in sel4 is even ten times more than that of the microkernel implementation itself @xcite . therefore, in order to promote provable software, automated software verification, particularly automated proof, is highly desirable. as an early exploratory effort, in this paper, we explore to automate the major overhead. typically, automated proof in software verification is a conditional generation task from the specification to the proof, involving reasoning capabilities. fortunately, large language models (llms) offer an opportunity, as they have demonstrated significant capacity in logic and reasoning at mathematical theorem proving @xcite @xcite . only limited re-figure 1 : a demonstration of the selene pipeline for automated proof generation (best viewed in color). selene facilitates both the construction of proofs from scratch (indicated by the gray "generate" path) and the refinement of existing proofs augmented by error messages (highlighted by the red "fixing" path). to validate the correctness of the generated proofs, they are subjected to verification by the isabelle prover within the authentic sel4 environment. we evaluate gpt-3.5-turbo (openai, 2023a) and @xcite in the selene pipeline. the experimental results demonstrate the feasibility of llms for automated proof in software verification. still, we have identified some further challenges in selene. ❶ the dependency graph of sel4 is complicated, and extracting facts to be applied from it can be hard for llms. ❷ the logic and reasoning process of a rather large proof may be beyond the capability of the subject llms. even gpt-4 has difficulty in solving the rather difficult categories in selene. therefore, to address the challenges, we introduce three distinct augmentations, i.e., similar lemma augmentation, dependency augmentation and fixing augmentation. these augmentations yield varying improvements across the selene's different categories. despite the inherent difficulties, our experimental results with these augmentations offer promising indications that the challenges posed by selene are surmountable. the main contributions of this paper can be summarized as below. ## selene we present the selene benchmark in this paper (figure 1 ), and evaluate llms' capabilities upon automated proof generation. the subject llm's goal is to write proofs for the given specifications from sel4 and pass the verification. however, the verification process in the original sel4 environment is time-consuming. given the impracticality of waiting for dozens of minutes to verify a single proof generated by the llm, we construct selene to align with the objective of lightweight evaluation. drawing on the session design in isabelle and sel4 (section 3.1), we introduce lemma isolation (section 3.2), which enables rapid verification of the target lemma (usually a few seconds). due to the complexity of sel4, we further delve into some specific implementation details of selene in section 3.3. ## augmentation as previously discussed, llms exhibit significant potential for automated proof when evaluated against selene, however, it is also evident that the task presents substantial challenges. we propose some augmentation techniques and evaluate them in our evaluation pipeline, with the aspiration that they may serve as a catalyst for further exploration in future studies. ## conclusion in this paper, we study the domain of automated proof within the context of software verification. we introduce selene, which is a real-world industrial-level automated proof benchmark derived from the sel4 project. selene provides a lightweight verification environment facilitated by lemma isolation with isabelle sessions. the current framework supports end-to-end proof generation and evaluation, bolstered by supplementary augomentation. by evaluating against advanced llms such as gpt-3.5-turbo and gpt-4, we demonstrate the potential of llms in automated proof generation for software verification. nevertheless, selene poses formidable challenges that llms have yet to overcome fully. it is our hope that selene will catalyze further research in this area, promoting advancements in software verification.