Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents

• 类型：arxiv
• 标识：2609.04043
• 链接：http://arxiv.org/abs/2609.04043v1
• 主分类：agent
• 形态：method
• 被引：0
• 被引来源：Semantic Scholar + OpenAlex
• S2被引：0
• OpenAlex被引：0
• 影响力被引：0
• TLDR：An application-level theorem is proved: if the user types echo hello world as input on the UART console, the only output the system can produce is hello world, which proves LLM-based agents are capable of reasoning about such low-level details.
• OpenAlex ID：W7208707327
• OpenAlex DOI：10.48550/arxiv.2609.04043
• DOI：10.48550/arxiv.2609.04043
• DOI来源：OpenAlex
• 开放获取：green
• 开放获取链接：https://doi.org/10.48550/arxiv.2609.04043
• OpenAlex更新：2026-09-06
• 待LLM分类：否
• 标题中文：将并发分离逻辑扩展到硬件层面，借助 AI Agent 在 RISC-V 上验证 xv6 OS 内核
• TLDR中文：证明了一个应用层定理：若用户在 UART 控制台输入 echo hello world，系统唯一能产生的输出即为 hello world；这证明了基于 LLM 的 Agent 能够对如此底层的细节进行推理。
• 来源文件：
• /inbox/tom/_candidates/2026-09-04-agent-rag-longcontext-candidates.json
• [OpenAlex backfill]
• [S2 enrich]