Neuro-Symbolic Proof Generation for Scaling Systems Software Verification

TL;DR

This paper presents a neuro-symbolic framework that combines large language models and symbolic tools to automate proof generation in system software verification, significantly improving scalability and proof success rates.

Contribution

The paper introduces a novel neuro-symbolic proof generation system that integrates LLMs with ITP tools for scalable, automated system verification, surpassing previous approaches.

Findings

Proves up to 77.6% of theorems on seL4 benchmark.

Outperforms previous LLM-based approaches and standalone Sledgehammer.

Demonstrates strong generalization across Isabelle benchmarks.

Abstract

Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models (LLMs), especially in mathematical reasoning, make their integration into software verification increasingly promising. This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for system-level verification projects. The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step. On the neural side, we fine-tune LLMs using datasets of proof state-step pairs; on the symbolic side, we incorporate a range of ITP tools to repair rejected steps, filter and rank proof states, and automatically discharge subgoals when search progress stalls. This synergy enables data-efficient LLM adaptation and semantics-informed pruning of the search space. We implement the framework on a new Isabelle REPL that exposes fine-grained proof states and automation tools, and evaluate it on the FVEL seL4 benchmark and additional Isabelle developments. On seL4, the system proves up to 77.6\% of the theorems, substantially surpassing previous LLM-based approaches and standalone Sledgehammer, while solving significantly more multi-step proofs. Results across further Isabelle benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.