Ochránce (Czech: protector, defender, guardian; pronounced OH-khran-tseh)
is a modular verification framework for subsystem integrity using dependent types
(Idris2). This file backs up the claims in the README. Note: the active
implementation repository is ochrance;
this ochrance-framework repo defines the abstract multi-subsystem interface
that the implementation and future subsystem modules implement against.
Dependent type proofs — verification backed by mathematical certainty, not just hash comparison. The same VerifiedSubsystem interface works for filesystems, memory, networks, and crypto.
The core contract is defined in
ochrance-core/Ochrance/Framework/Interface.idr. The VerifiedSubsystem
interface is parameterised by the subsystem implementation type sub and
requires three total functions: verify (pure, returns Either OchranceError
(VerificationProof mode SubState SubManifest)), repair (IO-bound, restores
from a snapshot), and attest (IO-bound, generates a fresh manifest from live
state). The VerificationProof type in Framework/Proof.idr is a GADT
indexed by VerificationMode (Lax / Checked / Attested) — this means the
compiler enforces that a Lax proof cannot be used where an Attested proof is
required. All parser and verification functions carry %default total,
enforcing Idris2’s totality checker. The verifyOrRepair pipeline in
Interface.idr composes these: attempt verify, on failure execute repair,
re-verify.
Caveat: The framework is ~10% implemented. The Filesystem module
(in ochrance-core/Ochrance/Filesystem/) is the furthest along (NVMe block
verification, Merkle trees, A2ML manifest parsing) and lives in the companion
ochrance repo at ~80% complete.
The Memory, Network, and Crypto module directories are skeletal — designed
but not yet implemented. Do not use this framework repo as evidence of
four working subsystems; it is an interface contract and partial scaffold.
-
Core interface:
ochrance-core/Ochrance/Framework/Interface.idr -
Proof types:
ochrance-core/Ochrance/Framework/Proof.idr -
Progressive modes:
ochrance-core/Ochrance/Framework/Progressive.idr -
Error types:
ochrance-core/Ochrance/Framework/Error.idr -
A2ML parser:
ochrance-core/Ochrance/A2ML/Parser.idr(total, proven)
Progressive strictness — trade security for performance dynamically (Lax/Checked/Attested). Lax: <1% overhead, structure only. Checked: ~2-5%, hash verification. Attested: ~10%, full dependent type proofs.
Progressive.idr defines VerificationMode as a data type with three
constructors. The verify function in VerifiedSubsystem takes mode as
an explicit argument, and VerificationProof is indexed by that mode — so
the proof you get back carries its verification level in its type. A Lax
verification produces a StructureValid witness; a Checked verification
adds hash comparison (BLAKE3); an Attested verification produces a full
dependent-type proof requiring hash match plus cryptographic attestation
signature. This typing prevents silent mode downgrade: code expecting
VerificationProof Attested s m will not type-check when handed a
VerificationProof Lax s m.
Caveat: The overhead figures (<1%, ~2-5%, ~10%) are design targets
documented in the README, not yet benchmarked against a running implementation
in this repo. Benchmark evidence will come from the ochrance implementation
repo once the Filesystem module reaches completion.
-
Mode definition:
ochrance-core/Ochrance/Framework/Progressive.idr -
Proof GADT:
ochrance-core/Ochrance/Framework/Proof.idr
|
Important
|
|
| Technology | Also Used In |
|---|---|
Idris2 for formal proofs |
stapeln (crypto proofs, 14/26 proven), ephapax (linear type proofs, 27 Qed / 3 Admitted), Groove protocol ABI definitions |
Thin C FFI pattern (Idris2 → C) |
|
ECHIDNA neurosymbolic integration |
echidna is the neural theorem-proving platform; Ochránce is a primary consumer of its Idris2 backend (13th prover) |
A2ML manifest format |
A2ML is the hyperpolymath-standard attestation and audit format; used in a2ml-showcase, standards, and all RSR repos |
| Path | What’s There |
|---|---|
|
The |
|
|
|
|
|
|
|
Shared type aliases, |
|
Repair strategy types and composition helpers. |
|
Merkle tree types for manifest representation. |
|
Verification pipeline helpers. |
|
Total lexer for the A2ML manifest format. Produces token stream. |
|
Total parser for A2ML. Accepts |
|
Serializes typed A2ML AST back to text. |
|
Validates A2ML semantic constraints (timestamp format, hash prefixes). |
|
Filesystem subsystem module (skeletal; full implementation in ochrance repo). |
|
Future subsystem modules. Design documented, not yet implemented. |
|
Thin C shims for NVMe syscalls via libnvme. <300 lines total. No business logic. Called by the Filesystem module’s Idris2 FFI declarations. |
|
Module-level documentation: |
|
Architecture overview, A2ML spec ( |
|
Idris2 package manifest. Declares all module paths for the compiler. |
|
Build recipes: |
|
Chainguard-based container for the framework tools. |
|
A2ML checkpoint files: STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK. |
# Type-check all modules
just check
# Verify totality annotations are present
just check-totality
# Build Idris2 + C shims
just build
# Run test suite
just test
# Check SPDX headers
just spdx-checkThis framework repo (ochrance-framework) defines the abstract architecture:
the VerifiedSubsystem interface and the four planned subsystem modules.
The ochrance repo is the concrete
reference implementation of the Filesystem module (~80% complete). They are
complementary: ochrance proves the approach works for one subsystem;
ochrance-framework provides the interface that future subsystem implementations
(Memory, Network, Crypto) will conform to.