Master Thesis - Experiment Results: LLM-Assisted Generation of Formal Verification Harnesses for the Intel TDX Module Firmware

LAHG (LLM-Assisted Harness Generator)

LAHG allows the semi-automatic generation of formal verification harnesses that are compatible with HarnessForge to reduce the cost of creating benchmark datasets for SV-COMP.

It uses Gemini CLI to generate the harnesses and employs an MCP Server to compile and validate these artifacts.

It requires a context injection in form a rule set, which can be generated for any new repository.

Prerequisites

For reproducibility, use these versions:OS: WSL2 Ubuntu on Win11Tools:

Clang for Windows x64: LLVM-18.1.8    Target: x86_64-pc-windows-msvc    Thread model: posix

HarnessForge 1.3.0-dev

CBMC version 6.7.1 (cbmc-6.7.1) 64-bit x86_64 linux

Gemini:

Gemini CLI 0.33.2 with gemini-3-flash

Gemini API Model: gemini-3-flash

Embeddings: text-embedding-001Code Base:

Intel TDX 2.0.08 (August 2025)

Contents

This dataset contains the following:

Zipped LAHG source code (lahg.zip)

Guide for Harness Generation to recreate experiments

Experiment data for all three experiments, that were conducted to evaluate LAHG's performance.

We conducted three experiments.The results of the first, along with all measurements, the raw data, and the plots are contained in experiment_1_results.zip and experiment_1_plots.zip.This also holds for experiments 2 and 3 for experiment_2.zip and experiment_3.zip.