# KaPilot — LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
> Ficha editorial pública de Research IA. Estado: Lectura primaria completa. La interpretación editorial no sustituye la fuente primaria.

- Página canónica: https://luiseduardodemiguel.com/research-ia/papers/kapilot-llm-assisted-generation-of-kani-specifications-for-unsafe-rust-v
- Fuente primaria: https://arxiv.org/abs/2607.21957
- Versión leída: v1
- Fuente comprobada: 2026-08-19 · lectura primaria completa; extracción editorial automatizada, revisión humana pendiente
- Autores: Minghua Wang, Yuxi Ling, Mingzhi Gao, Yuwei Liu, Lin Huang
- Fecha del corte: 24 JULIO 2026.
- Área: AGENTES · SEGURIDAD

## Tesis y contexto

Sistema multiagente que genera especificaciones formales para verificar código unsafe de Rust con Kani. Agentes separados extraen requisitos de seguridad, generan especificaciones, hacen prechecks y verifican/refinan los candidatos. Logra especificaciones verificables en 88,9% de funciones con ground truth y 71,4% sin él.

- Problema: La verificación formal es potente, pero escribir especificaciones manualmente es uno de sus mayores cuellos de botella.
- Por qué importa: Puede ser un puente entre LLMs probabilísticos y garantías formales.

## Evidencia reportada

- **reported-result**: 6 shows the performance of KaPilot against AutoSpec in terms of specification quality on GoldSet benchmark. [localizador](https://arxiv.org/html/2607.21957#S4)
- **reported-result**: In particular, KaPilot substantially reduced unsuitable preconditions, which include both incorrect and overly restrictive ones, by about 74% compared with AutoSpec. [localizador](https://arxiv.org/html/2607.21957#S4)
- **reported-result**: KaPilot generated around 22% fewer incorrect or overly weak postconditions, indicating better semantic alignment with the intended safety requirements. [localizador](https://arxiv.org/html/2607.21957#S4)
- **reported-result**: As a result, KaPilot reduced verification failures by approximately 57% relative to AutoSpec. [localizador](https://arxiv.org/html/2607.21957#S4)

## Lectura y límite

- Método: La lectura de 3. Approach describe la intervención y su construcción: We propose KaPilot , a multi-agent framework to automate the specification generation for unsafe Rust programs in Kani. Fig. 2 shows the overview of KaPilot . It takes the source code of the target functions and their documentation as inputs. In the preparation stage, it first extracts metadata from the source code via lightweight program analysis, including function signatures, call graph, and function description. Then, agent HarnGen constructs a Kani proof harness for the target function (details in Sec. 3.2 ). Meanwhile, SafetyReq extracts safety requirements based on the documentation written in natural…
- Límite: La lectura primaria permite comprobar método y resultados en el HTML, pero no convierte sus conclusiones en validación independiente. La ficha no demuestra transferencia fuera de los datasets, modelos, herramientas y condiciones descritos en 4. Evaluation.
- Confianza editorial: Media
- Limitación: El cierre de la fuente señala: Threat to validity. The ULSet dataset poses no risk of data leakage, as it contains no existing specifications. For the functions in GoldSet with human-written ground truth, a potential risk exists because the models’ training data are undisclosed. However, the knowledge cutoffs of GPT-5, Claude-Sonnet-4 and DeepSeek-v3.2 are September 2024, March and September 2025, respectively, at which time Kani specifications were scarce. Moreover, during our…
- Limitación: La ficha no demuestra transferencia fuera de los datasets, modelos, herramientas y condiciones descritos en 4. Evaluation.

## Localizadores de evidencia
- [Fuente primaria · canonical](https://arxiv.org/abs/2607.21957): tipo abstract
- [HTML · lectura completa](https://arxiv.org/html/2607.21957): tipo abstract
- [Método · 3. Approach](https://arxiv.org/html/2607.21957#S3): tipo section
- [Evaluación · 4. Evaluation](https://arxiv.org/html/2607.21957#S4): tipo section
- [Cierre · 5. Discussion](https://arxiv.org/html/2607.21957#S5): tipo section

## Próxima prueba

- ¿La propuesta mejora secure coding frente a la línea base actual?
- Métrica: Comparar la métrica principal de la fuente junto con calidad, coste, latencia y tasa de errores.
- Regla de parada: Parar si no aparece una mejora reproducible o si aumenta el riesgo, la complejidad o el coste sin compensación.

## Recursos reproducibles
- [Link](https://project-oak.github.io/rust-verification-tools/about.html)
- [the following issues](https://github.com/arXiv/html_feedback/issues)
- [list of packages that need conversion](https://github.com/brucemiller/LaTeXML/wiki/Porting-LaTeX-packages-for-LaTeXML)
- [developer contributions](https://github.com/brucemiller/LaTeXML/issues)

## Enlaces relacionados

- [VAKRA](https://luiseduardodemiguel.com/research-ia/markdown/papers/vakra)
- [The Devil Is in the Interface](https://luiseduardodemiguel.com/research-ia/markdown/papers/devil-interface)
- [SkillSentry](https://luiseduardodemiguel.com/research-ia/markdown/papers/skillsentry)