SakuraOS Bootloader

A formally verified, multi-architecture bootloader implemented in Pure SPARK/Ada. Safe, secure, and mathematically proven correctness from the very first instruction.

Supported Architectures

Designed to be consistent across x86_64 (UEFI & Legacy BIOS), AArch64 (UEFI), and RISC-V 64-bit.

Formal Verification

Verification targeted by subsystem (Gold/Silver levels). SPARK contracts enforce valid state transitions and memory safety.

Architecture & Design

The bootloader sits between the firmware (UEFI/BIOS) and the SakuraOS Kernel. It is driven by a strictly defined Boot Phase State Machine that enforces valid transitions from initialization to kernel handoff.

Firmware Abstraction: Clean separation between UEFI bindings and core logic.
Error Handling: No exceptions. Deterministic error propagation compatible with Ravenscar/SPARK.
Boot Protocol: Custom handoff protocol passing memory maps, ACPI/DTB pointers, and security context.

Security Model

Security is not an afterthought but a foundational requirement.

Secure Boot integration (UEFI context)
Hybrid Post-Quantum Cryptography (ML-DSA + Classical)
SKI: SakuraOS Kernel Image format with encryption
Zero usage of C libraries (Pure Ada/SPARK)

Verification Status

The project follows a strict "SPARK-first" policy. SPARK_Mode => Off is restricted to minimal hardware interfaces.

Component	Status	Technique
State Machine	Verified	Flow Analysis & Contracts
Boot Protocol	Verified	Type Safety & Bounds Check
Crypto Subsystem	In Progress	Functional Correctness