Introducing Dezhan: Provably Immutable Backups

Most backup systems ask you to trust that data, once written, stays untouched. Dezhan is a new open-source project that takes a stronger position: its core immutability rules are not just tested, they are mathematically proven. It is an air-gapped, S3-compatible backup vault whose trusted core is written in Ada 2022 and SPARK, and whose safety invariants are machine-verified with a formal prover.

This is an early-stage project, built in the open. We think the idea is worth sharing now, because the approach is unusual and the bar it sets for backup integrity is high.

Why dezhan is different

The heart of dezhan is a small trusted core that enforces one non-negotiable rule:

Retention may be extended, never shortened, and a retained object cannot be deleted before its expiry.

That sentence is the whole point of an immutable vault, and it is exactly the kind of rule that quietly breaks under an edge case, a race, or a clever caller. In dezhan it is expressed as a SPARK contract and checked by gnatprove across every reachable state. The proof either holds for all inputs or the build fails. There is no "it passed the tests we thought to write."

• Provable, not just plausible. The integrity-critical invariants are formally verified, so a class of "the backup was silently mutable" bugs is ruled out by construction.
• Air-gapped by design. The vault is built to run isolated, mirroring how serious backup targets are actually deployed: offline, minimal surface, no outbound chatter.
• S3-compatible. It speaks the API your tooling already knows, so restic, Velero, the AWS CLI, and boto3 work against it without bespoke glue.
• Cloud-native. A Kubernetes operator and a CSI driver let you declare a vault and mount it the same way you manage everything else in your cluster.
• Small trusted base. SPARK covers the core; external dependencies sit behind a minimal, audited boundary, so the part you have to trust stays small enough to reason about.

Why this matters

Immutability is the property ransomware and accidental deletion both attack. The usual answer is policy and configuration: object-lock flags, retention settings, hopefully-correct IAM. Those help, but they are assertions, not guarantees. Dezhan moves the guarantee into the code itself and then proves the code obeys it. For compliance, ransomware recovery, and any "this data must survive untouched" requirement, a proof is a much stronger thing to stand behind than a test suite.

A young project, in the open

Dezhan is new and moving fast. The trusted core is being built and proven one unit at a time, the operator and CSI driver are usable today, and the roadmap is public. If formally verified immutability is interesting to you, this is a good moment to look, try it, and shape where it goes.