2 papers
cs.LO2026
Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents
M. Frans Kaashoek, Nickolai Zeldovich
MachCSL is a framework for verifying system 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 beh…
cs.DC2025
Shipwright: Proving liveness of distributed systems with Byzantine participants
Derek Leung, Nickolai Zeldovich, Frans Kaashoek
Ensuring liveness in a decentralized system, such as PBFT, is critical, because there may not be any single administrator that can restart the system if it encounters a liveness bu…