Ochránce

Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> v0.1.0, 2026-02-06 :toc: :icons: font :source-highlighter: rouge

Overview

Ochránce is a neurosymbolic filesystem verification framework built with Idris2 dependent types. It provides mathematically proven guarantees about filesystem integrity through:

• A2ML (Attestation & Audit Markup Language) - A formally specified markup for filesystem manifests

• Verified Merkle trees - Size-indexed binary trees with compile-time structure proofs

• Linear type repair - Filesystem repair operations that prevent use-after-repair bugs

• ECHIDNA integration - Neural proof synthesis for automated verification

Status

Formal verification is in progress — see docs/PROOFS.adoc for the authoritative, dependency-sorted plan and the currently-proven surface (combiner-generic Merkle soundness, A2ML parser totality, manifest round-trip, progressive assurance). Cryptographic integrity is not yet claimed: the real BLAKE3 / SHA-256 / SHA3-256 / Ed25519 lives in the Zig FFI, but the Idris-side stub fallbacks must be removed and libochrance.so linked into the verification flow first (issue #39).

Architecture

┌─────────────────────────────────────────────┐
│            Ochránce (Idris2)                │
│                                              │
│  A2ML Parser/Validator ←→ Merkle Trees      │
│         ↓                     ↓              │
│  VerifiedSubsystem Interface                 │
│         ↓                                    │
│  Filesystem Module (reference impl)          │
└──────────────┬──────────────────────────────┘
               │ C FFI
               ↓
┌──────────────────────────────────────────────┐
│          ECHIDNA (Rust/Julia)                │
│  Neural proof synthesis + Multi-prover       │
└──────────────────────────────────────────────┘

Quick Start

# Requires Idris2 0.8.0+
idris2 --build ochrance.ipkg

Verification Modes

Mode	Description
Lax	Parse manifest only, skip hash verification
Checked	Verify all block hashes match Merkle root
Attested	Checked + verify cryptographic attestation signature

Related Repositories

ochrance-framework (Parent Framework)

This repo is the reference implementation of the Filesystem module defined in the ochrance-framework repository.

The framework defines the broader VerifiedSubsystem interface and four planned subsystem modules (Filesystem, Memory, Network, Crypto). This repo (ochrance) provides the concrete, working implementation of the Filesystem module using Idris2 dependent types and Zig FFI.

The two repos are complementary:

• ochrance (this repo) — the canonical core: concrete filesystem verification with the machine-checked proofs and the Zig crypto FFI.

• ochrance-framework — the architecture / specification layer (the VerifiedSubsystem interface and the four planned subsystem modules). Its earlier duplicate core is retired in favour of this repo’s (decision D1).

valence-shell & echo-types (Reversibility Stack neighbours)

Ochránce can eventually act as the receipt layer for valence-shell's accountable state transitions, with echo-types supplying the semantics of the residue/loss those transitions expose. This relationship is documentation-only and not mechanised today — see docs/VALENCE_SHELL_BRIDGE.adoc (and its machine-readable companion .machine_readable/integrations/valence-shell-bridge.a2ml) for the trust boundaries and caveats.

License

This project is licensed under the Mozilla Public License, v. 2.0. See the LICENSE file for details.

SPDX-License-Identifier: CC-BY-SA-4.0

Topology & Dashboard

See TOPOLOGY.md for a visual architecture map and completion dashboard.