formal-validation-related.md

• seL4: Formal Verification of an OS Kernel

  • seL4 proj

• CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels

  • certikos proj

• A Practical Verification Framework for Preemptive OS Kernels

• Hyperkernel: Push-Button Verification of an OS Kernel

  • hyperkernel proj

• Scaling symbolic evaluation for automated verification of systems code with Serval

• Nickel: A Framework for Design and Verification of Information Flow Control Systems

• A Secure and Formally Verified Linux KVM Hypervisor

• Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware

  • sosp 2021 Artifact Review Summary