Skip to content

README.adoc

Latest commit

 

History

History
87 lines (63 loc) · 3.09 KB

README.adoc

File metadata and controls

87 lines (63 loc) · 3.09 KB

Ochránce

Table of Contents

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

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, not duplicates:

  • ochrance (this repo) — concrete filesystem verification implementation (~80% complete)

  • ochrance-framework — abstract modular framework for all four subsystems (~10% complete)

License

SPDX-License-Identifier: PMPL-1.0-or-later

Copyright © 2026 Jonathan D.A. Jewell. All rights reserved.

Architecture

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