Kagura File System

A high-reliability, user-space distributed file system. Merging SPARK correctness with modern ZFS-like storage features.

Transactional Copy-on-Write

All writes are grouped into Transaction Groups (TXG). Consistent state is guaranteed via on-disk CoW semantics using B+Trees and Uberblocks.

Advanced Cryptography

Built-in AEAD encryption and PQC hybrid key exchange (X25519 + ML-KEM-1024). Security is baked into the protocol, not an add-on.

System Architecture

Kagura FS operates primarily in user space, communicating via a clean IPC protocol. It uses a layered architecture designed for verification:

[VFS Layer]: Permissions, Handles, Path Resolution
↓
[Object Store]: Inodes, Directories, Attributes
↓
[B+Tree]: Generic Key-Value Storage
↓
[Transaction]: Consistency Management (TXG)
↓
[Block I/O]: Physical Device Access & RAID

KFS Protocol

Communication between the OS and Kagura FS uses a custom TLV-based protocol optimized for reliability and zero-copy performance.

Transfer Modes: INLINE (small data), SHM (zero-copy shared memory), STREAM (large data).
Flow Control: Window-based updates and heartbeats.
Session Security: Authenticated handshake using HKDF and hybrid PQC.

Proof & Quality

Kagura FS targets formal proof of critical properties, including data consistency and absence of runtime errors. The development process integrates GNATprove into the CI loop.