Vörðr

Formally verified container orchestration and verification system.

Guardian of containers. Watcher of states. Keeper of proofs.

The Name

Vörðr (Old Norse: /ˈvørðr/) means "guardian" or "watcher" — a spirit that follows and protects. In this system, Vörðr watches container lifecycles, guards state transitions, and ensures formal correctness through mathematical proof.

The ASCII-safe spelling is vordr.

The Languages

Vörðr is polyglot by design, using the right tool for each verification domain:

Language	Domain	Rationale
Idris2	Formal verification core	Dependent types enable proofs about container lifecycles as first-class values
Rust	eBPF runtime monitoring	Zero-cost abstractions for performance-critical syscall interception
Elixir	Orchestration & reversibility	BEAM’s fault tolerance + immutable state for Bennett-reversible operations
Ada/SPARK	Trust mechanisms	Contractual design + SPARK proofs for cryptographic operations

Who Is This For?

• Security engineers who need formal guarantees about container behavior

• DevOps teams requiring reversible, auditable container operations

• Researchers exploring neuro-symbolic AI for infrastructure decisions

• RISC-V enthusiasts deploying verified containers on edge hardware

Why Vörðr?

Multi-Stage Verification

┌─────────────┐    ┌─────────────┐    ┌─────────────┐
│   STATIC    │───▶│   DYNAMIC   │───▶│   FORMAL    │
│ (Manifests) │    │   (eBPF)    │    │  (Proofs)   │
└─────────────┘    └─────────────┘    └─────────────┘
     │                   │                   │
     ▼                   ▼                   ▼
  Idris2/ATS2      Rust/eBPF          Coq/Idris2
  Scan SBOMs      Monitor syscalls   Generate proofs

Reversible Operations

Every state transition is Bennett-reversible. Undo any operation:

vordr deploy --image nginx:latest    # Deploy container
vordr undo --last                    # Reverse deployment
vordr audit --chain                  # Show reversibility chain

Neuro-Symbolic AI Integration

MCP decisions are auditable through Flux.jl integration:

vordr audit-mcp --decision scale-up --explain
# Output: Proof that scaling decision satisfies safety constraints

RISC-V Native

Cross-compiles to StarFive VisionFive 2 and Jetson Nano:

vordr build --target riscv64gc-unknown-linux-gnu
vordr deploy --device jetson-nano --npu-accelerate

Quick Start

Prerequisites

• Idris2 (>= 0.6.0)

• Rust (>= 1.75.0) with riscv64gc-unknown-linux-gnu target

• Elixir (>= 1.16.0)

• GNAT (Ada compiler, >= 13.0)

Installation

git clone https://gitlab.com/hyperpolymath/vordr.git
cd vordr
just setup      # Install dependencies
just build      # Compile all components
just test       # Run verification suite

Basic Usage

# Verify a container image statically
vordr verify --static --image nginx:latest

# Monitor a running container with eBPF
vordr monitor --ebpf --container my-app

# Generate formal proofs of lifecycle compliance
vordr prove --lifecycle container_lifecycle.idr

# Full verification pipeline
vordr verify-all --image nginx:latest --prove --monitor

Architecture

                          ┌─────────────────────────────────────┐
                          │           VÖRÐR CORE                │
                          │  (Orchestration & Verification)     │
                          └──────────────┬──────────────────────┘
                                         │
         ┌───────────────────────────────┼───────────────────────────────┐
         │                               │                               │
         ▼                               ▼                               ▼
┌─────────────────┐           ┌─────────────────┐           ┌─────────────────┐
│    SVALINN      │           │   CERRO TORRE   │           │     OBLIBENY    │
│  (Edge Shield)  │◀─────────▶│ (Build Verify)  │◀─────────▶│  (Orchestrate)  │
│   [ReScript]    │           │  [Ada/SPARK]    │           │    [Elixir]     │
└────────┬────────┘           └────────┬────────┘           └────────┬────────┘
         │                             │                             │
         ▼                             ▼                             ▼
┌─────────────────┐           ┌─────────────────┐           ┌─────────────────┐
│   OCI Hooks     │           │  Attestations   │           │  State Machine  │
│   [Rust/eBPF]   │           │  [Sigstore]     │           │  [GenServer]    │
└─────────────────┘           └─────────────────┘           └─────────────────┘
         │                             │                             │
         └─────────────────────────────┼─────────────────────────────┘
                                       │
                          ┌────────────┴────────────┐
                          │      DATA LAYER         │
                          │                         │
                          │  ArangoDB  Dragonfly    │
                          │  (Attest)  (Cache)      │
                          │                         │
                          │        LMDB             │
                          │       (Proofs)          │
                          └─────────────────────────┘

Components

Component	Location	Description
Verification Core	src/idris2/	Formal verification of container lifecycles, policies, cryptographic operations
Runtime Monitor	src/rust/	eBPF-based syscall monitoring, anomaly detection, Sigstore integration
Orchestrator	src/elixir/	Bennett-reversible state machine, MCP integration, Borg backup coordination
Trust Engine	src/ada/	SPARK-proven threshold signatures, Gatekeeper policies, federated logs
MCP Adapter	adapters/	ReScript adapter for poly-ssg-mcp hub integration
WASM Runtime	runtime/	Browser/edge verification via Idris2→WASM compilation

Integration

With Svalinn (Edge Shield)

# Svalinn calls Vörðr for container verification
Vordr.verify(%Container{image: "nginx:latest", hooks: [:before_start]})

With Cerro Torre (Build Verification)

-- Cerro Torre generates attestations that Vörðr verifies
procedure Verify_Build_Attestation (Manifest : CTP_Manifest) is
   Proof : Idris_Proof := Vordr.Verify_CTP (Manifest);
begin
   pragma Assert (Proof.Valid);
end Verify_Build_Attestation;

With mustfile

See Mustfile for mandatory verification gates.

Part of the Hyperpolymath Ecosystem

Vörðr is part of the hyperpolymath constellation of formally verified, reversible infrastructure tools:

• Svalinn — Edge container shield (ReScript)

• Cerro Torre — Provenance-verified builds (Ada/SPARK)

• Oblibeny — Declarative orchestration (Elixir)

• mustfile — Reversible task orchestration (Guile Scheme)

• poly-ssg-mcp — MCP hub for all satellites

License

SPDX-License-Identifier: PMPL-1.0

Vörðr is free software under the GNU Affero General Public License v3.0 or later. See LICENSE.txt for full terms.