一句话：提出三阶段流水线，用持续细粒度 LLM 反馈将 RFC 自动提取为可验证 TLA+ 模型，并用 TLC 检测故障。
从 RFC 等自然语言协议规范中提取可形式验证的模型困难且依赖专家。现有 LLM 自动化方法存在结构不一致、幻觉和扩展性有限等问题。本文提出 RFC2TLA+，将提取分解为状态、迁移和不变式三遍，并通过细粒度工具调用、轻量校验与迭代反馈向 LLM 提供持续反馈，以尽早纠错并减少语法与语义不一致。所得通信有限状态机被确定性翻译为 TLA+，由 TLC 模型检测器验证。在 14 个 RFC 及人工 FSM 基准上，RFC2TLA+ 生成比基线更完整的模型，并能提取不变式以检测注入故障；合成 RFC 实验也验证了其提取与检错效果。
Extracting natural-language protocol specifications such as Requests for Comments (RFCs) into formally verifiable models is a challenging and labor-intensive process that requires significant expertise. Recent advances in large language models (LLMs) and agents show promise in automating this task. However, existing automated approaches suffer from insufficient structural consistency, hallucinations, and limited scalability. Moreover, the ability to pass such automatically extracted models into formal verification tools such as model checkers has not been demonstrated. We present RFC2TLA+, a three-stage pipeline for automatically extracting RFCs into automatically verifiable models. RFC2TLA+ achieves this by providing fine-grain and continuous feedback to the LLM throughout the extraction process. It decomposes the extraction process into three passes—states, transitions, and invariants—while constraining LLM generation through fine-grained tool calls, lightweight validation, and iterative feedback. This design enables early error detection and correction, mitigating hallucinations and preventing syntactic and semantic inconsistencies. The resulting communicating finite-state machines (CFSMs) are deterministically translated into TLA + and verified using the TLC model checker. We evaluate RFC2TLA+ on a benchmark of 14 RFCs and their accompanying human-crafted FSMs and show that it generates more complete models than the baseline. In addition, our tool extracts invariants, enabling a model checker to detect injected faults. To minimize the effects of LLM memorization, we additionally generate synthetic RFCs and evaluate the tool on them, demonstrating its effectiveness in both model extraction and error detection.
@inproceedings{paperbot12340,
title = {RFC2TLA+: Extracting and Verifying Formal Models from RFC Documents using Continuous LLM Feedback},
author = {Guozhen Ding and Kexin Li and Ilya Grishchenko and David Lie},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3837453}
}