# KerSpecGen: Co-piloting formal Kernel specification synthesis with refined knowledge graphs and large language models

## TL;DR

KerSpecGen uses AI and knowledge graphs to automate the creation of formal software kernel specifications, reducing the need for manual expert work.

## Contribution

The first framework to generate formal specifications for complex microkernels using LLMs and refined knowledge graphs.

## Key findings

- KerSpecGen outperforms Few-shot methods by 7.06 percentage points in BLEU-4 on a seL4 benchmark.
- For Llama-3.1-405B, KerSpecGen produces better specifications in 23 out of 30 functional modules.
- The framework generates high-quality reference specifications requiring only minor adjustments for execution.

## Abstract

Formal verification ensures software correctness but faces challenges in kernel specification writing, which is labor-intensive, expertise-dependent, and limited to specific targets. For complex microkernels like seL4, these issues significantly reduce the practicality of formal methods. To address this, we propose KerSpecGen, a Large Language Model (LLM) based framework for synthesizing formal kernel specifications, which leverages knowledge graphs to bridge requirement descriptions and specification properties.

KerSpecGen’s core design includes three key components: 1) constructing a refined knowledge graph to represent progressive specification relationships (with deduplication, property judgment, and source annotation to improve accuracy); 2) building a custom dataset to fine-tune a model that converts specification properties into code; 3) designing LLM-oriented synthesis templates to transform generated code into complete candidate specification programs.

Evaluation on our KerSpecProperty benchmark (30 seL4 function modules, 624 properties) shows KerSpecGen outperforms the Few-shot method by an average of 7.06 percentage points in BLEU-4. Specifically, for the Llama-3.1-405B model, KerSpecGen achieves better specification quality than the Few-shot method in 23 out of 30 functional modules. To our knowledge, this is the first work to generate formal specifications for complex microkernels. KerSpecGen yields high-quality reference specifications. While requiring minor adjustments for direct execution, it substantially reduces the burden of writing specifications from scratch.