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
• TLDR：MachCSL is a framework for verifying systems software, such as an OS kernel, on top of low-level semantics of a RISC-V computer, based on the Sail RISC-V semantics. The key idea behind MachCSL is to adapt concurrent separation logic, based on Iris, to reasoning about low-level hardware execution at the sub-instruction level: page-table translation, TLB, privilege levels, configuration registers, instruction fetch/decode/execute, traps and interrupts, DMA, shared memory, power failures, etc. Reasoning at this level of detail ensures that the system software correctly manages all of the hardware
• 待LLM分类：否
• 来源文件：
• /inbox/tom/_candidates/2026-09-04-agent-rag-longcontext-candidates.json