Research map / Large language models / Agents, code and math
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes FVEL, an interactive environment that translates C code into Isabelle and verifies it via LLM-driven theorem proving, plus the FVEL dataset extracted from seL4 proofs, and LoRA fine-tunes Llama-3-8B and Mistral-7B on it.
Problem
Current formal verification of code relies on symbolic verifiers or hand-crafted rules that limit flexible verification, while LLMs' formal reasoning ability in interactive theorem proving remains underexplored for code verification.
Approach
Transform C code into Isabelle definitions (via C-Parser and AutoCorres) and let an LLM generate lemma specifications and step-wise proofs interacting with the Isabelle prover through PISA, with feedback from the prover; supported by a large dataset of seL4 theories, lemmas and proof steps.
Key results
- Llama3-8B-FT solves 81 vs 69 base on SV-COMP-1000 (17.39% gain).
- Mistral-7B-FT solves 84 vs 75 base on SV-COMP-1000 (12% gain).
- On the FVEL test split, fine-tuned Mistral-7B and Llama-3-8B reach 6.9% and 8.1% pass rates, up from 2.4% and 3.6%.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Fine-tune Mistral-7B on FVELER | Mistral-7B in FVEL · SV-COMP (1,000) | verified tasks: 75 -> 84 | Helped |
| Fine-tune Llama3-8B on FVELER | Llama3-8B in FVEL · SV-COMP (1,000) | verified tasks: 69 -> 81 | Helped |
| Fine-tune Mistral-7B on FVELER | Mistral-7B in FVEL · Code2Inv | verified tasks: 37 -> 40 | Helped |
| Fine-tune Llama3-8B on FVELER | Llama3-8B in FVEL · Code2Inv | verified tasks: 46 -> 46 | No clear effect |
| Fine-tune Mistral-7B on FVELER | Mistral-7B in FVEL · SV-COMP-47 | verified tasks: 10 -> 14 | Helped |
| Fine-tune Llama3-8B on FVELER | Llama3-8B in FVEL · SV-COMP-47 | verified tasks: 11 -> 16 | Helped |
| Fine-tune Mistral-7B on FVELER | Mistral-7B in FVEL · SV-COMP | proof error (%): 50.3 -> 41.0 | Helped |
| Fine-tune Llama3-8B on FVELER | Llama3-8B in FVEL · SV-COMP | proof error (%): 47.0 -> 38.2 | Helped |
| Fine-tune Mistral-7B on FVELER | Mistral-7B in FVEL · Code2Inv | statement error (%): 70.8 -> 72.0 | Hurt |
| Fine-tune Llama3-8B on FVELER | Llama3-8B in FVEL · Code2Inv | statement error (%): 67.8 -> 66.7 | Helped |
| Fine-tune Mistral-7B on FVELER | Mistral-7B in FVEL · FVELER test split | proof correctness (%): 2.4% -> 6.9% | Helped |
| Fine-tune Llama-3-8B on FVELER | Llama-3-8B in FVEL · FVELER test split | proof correctness (%): 3.6% -> 8.1% | Helped |
Surprising findings
- Symbolic solvers (UAutomizer with 374 of 1,000) still dominate the SV-COMP-1000 benchmark over the LLM-based approaches.
- Absolute pass rates on the FVEL test sets remain low (under 9%), indicating the benchmark is hard for current LLMs.
Limitations
- Only C code verification is supported; extension to other languages is future work.
- Semantic alignment between lemma statements and program specifications is unexplored.
- Absolute pass rates are low, limited by data scarcity in formal verification.
Experimental setup
Datasets: FVEL dataset (seL4-derived Isabelle theories, lemmas, proof steps) Code2Inv SV-COMP
Benchmarks: Code2Inv SV-COMP-47 SV-COMP-1000 FVEL test FVEL test-hard
Metrics: number of problems passed proof error proportion statement error proportion pass rate
Baselines: UAutomizer ESBMC Lemur-GPT-3.5-turbo Lemur-GPT-4 Mistral-7B Llama3-8B
Builds on: PISA Lemur LoRA AutoCorres C-Parser
Closest papers by meaning
- Neural Theorem Proving for Verification Conditions: A Real-World Benchmark (ICLR 2026 · similarity 0.90)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.89)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.88)
- Lemur: Integrating Large Language Models in Automated Program Verification (ICLR 2024 · similarity 0.87)
- HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs (ICML 2026 · similarity 0.87)
- Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization (ICLR 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.