SakuraOS

A capability-based microkernel, built from scratch and formally verified using SPARK/Ada. Elimination of runtime errors by mathematical proof.

Sponsorship Inquiry

gnatprove --version

$ gnatprove -P sakura_os.gpr
Phase 1 of 2: generation of Global contracts...
Phase 2 of 2: analysis of data and information flow...
Summary of formal verification:
--------------------------------------------------
Total proofs:          1248
Passed:                1248 (100%)
Failed:                0
Time spent:            01h 14m 22s
--------------------------------------------------

PROJECTS

Four pillars of SakuraOS

A quick overview. Detailed technical writeups are on each component page.

View progress ->

MICROKERNEL

SakuraOS Kernel

Capability-based core with SPARK-first verification.

Read details ->

BOOTLOADER

Secure Boot Flow

Multi-arch bootloader with verifiable handoff.

Read details ->

FILESYSTEM

Kagura FS

Copy-on-write storage with modern cryptography.

Read details ->

VIRTIO

SPARK Drivers

High-assurance I/O stack for VirtIO 1.4.

Read details ->