Oblíbený

Secure edge language for reversibility and accountability in hostile environments.

Oblíbený (Czech for "favorite" or "beloved") is a dual-form programming language that guarantees termination through Turing-incompleteness while maintaining full reversibility and complete accountability. Built for deployment in hostile environments where formal guarantees are essential.

Status: Active Development

CI-gated since 2026-06 — the language toolchain is functional: OCaml build, the 27-test conformance suite, and the Idris2 ABI proof layer (genuine total proofs since PR #51, no believe_me/postulate) are all gated in CI (PR #52). Honest open items: the Zig crypto FFI compiles (Zig 0.13, PR #56) but links only where the external liboqs library is installed; the obli-pkg signature-verify path is an explicit MVP stub (TODO(security)); see .machine_readable/6a2/STATE.a2ml for the live blocker list.

Component	Status	Description
Compiler & Runtime	✅ 100%	OCaml compiler with lexer, parser, type checker, evaluator, constrained form validator
Static Analyzer	✅ 100%	Resource bounds tracking, reversibility checking, trace coverage analysis
LSP Server	✅ 100%	Language Server Protocol with diagnostics, hover, completion (789 LOC)
Debugger	✅ 100%	Reversible debugger with forward/backward stepping, checkpoint inspection
Profiler	✅ 100%	Performance profiling with resource bounds, efficiency analysis, bottleneck detection
VSCode Extension	✅ 100%	Syntax highlighting, reversible op highlighting, invalid keyword detection
Echo Residue Type	✅ 100%	First-class echo[A, B] type: structured, proof-relevant residue of irreversible collapse; content-sensitive linearity discipline (non-copyable echoes consumed exactly once, PR #55)
Documentation	✅ 100%	Language specification, tutorial, security model, API reference, EXPLAINME, contractiles, echo-6a2 spec
Crypto FFI	⚠️ Compiles	Post-quantum crypto (liboqs + libsodium) via Zig FFI with Idris2 ABI proofs; compiles under Zig 0.13, links only with system liboqs; obli-pkg verify path is an MVP stub (TODO(security))
Deployment	✅ 100%	Svalinn/Vordr verified container stack with formal verification

Unique Features

Dual-Form Architecture

Oblibený separates compile-time and runtime concerns:

// Factory Form (Turing-complete, compile-time)(define(generate-loop n)(emit `(for i in0..,(const n){trace("iteration", i);})))// Constrained Form (Turing-incomplete, runtime)fnmain() -> (){checkpoint("start");for i in0..10{// Static bound requiredtrace("iteration", i);}checkpoint("end");}

Guaranteed Termination

Theorem: All valid constrained form programs terminate.

Enforcement: - ❌ NO while or loop keywords (rejected by parser) - ❌ NO recursive function calls (enforced by call graph checker) - ✅ ONLY bounded iteration: for i in 0..N where N is static - ✅ Acyclic call graph guaranteed

Complete Reversibility

Every operation has a well-defined inverse:

incr(x,5);// Inverse: decr(x, 5)swap(a, b);// Self-inverse
x ^= val;// Self-inverse (XOR)

Reversible debugger can step backward through execution!

Full Accountability

Every operation produces an immutable audit trail:

checkpoint("start");trace("event", arg1, arg2);assert_invariant(condition,"message");checkpoint("end");

Traces are cryptographically hashed for integrity.

Echo Residue Type

The type-level dual of the reversible core. Where a computation cannot be reversed, it can still retain a structured echo of what was lost:

// Parity collapse: distinct sources (7, 9) → same visible (1)// but the witness retains the original source valuefncollapse(n:i64) -> echo[i64, i64]{returnecho(n, n % 2);}fnmain() -> (){let a:echo[i64, i64] = collapse(7);let b:echo[i64, i64] = collapse(9);// Same observation survived (both odd)assert_invariant(echo_visible(a) == echo_visible(b),"same parity");// Witnesses tell the sources apartassert_invariant(echo_witness(a) != echo_witness(b),"distinct sources");}

Form	Syntax	Meaning
Type	echo[A, B]	Residue of a collapse A → B
Introduction	echo(source, base)	Form a residue
Elimination	echo_visible(e) : B	The surviving observation
Elimination	echo_witness(e) : A	The retained source constraint

Linearity discipline: echo[A, B] is linear (consumed exactly once) if and only if A or B is non-copyable. echo[i64, i64] projects freely; echo[Cargo, i64] is consumed on first projection, and discarding it unconsumed (overwrite or drop) is a type error — an irreversible step must account for an echo of what it loses (PR #55).

This realises, in a non-dependent constrained language, the echo-types fibre Echo f y := Σ (x : A), f x ≡ y from hyperpolymath/echo-types (Agda). See docs/echo-alignment.md and docs/specs/echo-6a2.adoc for the ecosystem alignment decisions.

Installation

Prerequisites

# Fedora/RHEL
sudo dnf install opam ocaml-dune ocaml-menhir
# Build dependencies
opam install dune menhir sedlex yojson ppx_deriving ppx_deriving_yojson alcotest
# Crypto libraries (for FFI)
sudo dnf install libsodium-devel

Build from Source

git clone https://github.com/hyperpolymath/oblibeny.git
cd oblibeny
dune build
dune install

Verify Installation

oblibeny --version
oblibeny-lsp --version

Quick Start

Hello World

Create hello.obl:

fnmain() -> (){checkpoint("start");trace("message","Hello, Oblíbený!");checkpoint("end");}

Run:

oblibeny hello.obl

Fibonacci (with Static Bounds)

fnmain() -> (){letmut a:i64 = 0;letmut b:i64 = 1;checkpoint("start_fibonacci");// Bounded iteration with static Nfor i in0..10{trace("fib", a);let tmp:i64 = a + b;
a = b;
b = tmp;}checkpoint("end_fibonacci");assert_invariant(a == 55,"10th Fibonacci should be 55");}

Static Analysis

oblibeny --analyze fibonacci.obl

Output:

=== Oblíbený Static Analysis Report ===
## Constrained Form Validation
✓ VALID - Program conforms to Turing-incomplete constrained form
## Resource Bounds (Static Guarantees)
Max loop iterations: 10
Max call depth: 0
Estimated memory: 24 bytes
## Reversibility Analysis
✓ All reversible operations are properly balanced
## Accountability Trace Coverage
Coverage: 40.0%

CLI Reference

oblibeny input.obl # Compile and execute
oblibeny --check input.obl # Validate constrained form only
oblibeny --analyze input.obl # Static analysis with resource bounds
oblibeny --dump-ast input.obl # Show parsed AST
oblibeny --dump-trace input.obl # Show accountability trace
oblibeny -v input.obl # Verbose output

Reversible Debugger

oblibeny --debug program.obl

Commands:

s, step - Step forward
b, back - Step BACKWARD (reversible!)
p, print - Show current state
t, trace - Show accountability trace
c, continue - Run to next checkpoint
h, help - Show help
q, quit - Exit debugger

Formal Verification

Oblibeny integrates with:

• Idris2: ABI proofs for FFI safety (src/abi/*.idr) — genuine total proofs, machine-checked in CI with an escape-hatch guard (no believe_me/postulate; PRs #51/#52)

• Zig: Memory-safe FFI implementation (ffi/zig/)

• Vörðr: Runtime verification with formal proofs

Verified properties: - ✓ Termination guaranteed - ✓ Resource bounds computable statically - ✓ Call graph is acyclic - ✓ No unbounded loops - ✓ Reversible operations correct

Deployment

Svalinn/Vordr Stack (Recommended)

# Build with formal verification
svalinn-compose build
# Deploy LSP server (2 replicas)
svalinn-compose up
# Scale analyzer/debugger on-demand
svalinn-compose up --scale analyzer=1

See svalinn-compose.yaml for full configuration.

Standalone Container

podman build -f Containerfile -t oblibeny:latest .
podman run -p 8765:8765 oblibeny:latest

Documentation

• EXPLAINME - What Oblíbený is, why it exists, and why it matters (start here)

• Language Specification - Complete grammar and semantics

• Tutorial - Step-by-step guide with examples

• Examples - 10+ example programs

• Core Specification - Formal specification in Scheme

• Contractiles - Formal behavioral contracts and invariants

• Echo Interface Spec §6.a.2 - Echo-types external interface contract

• Echo Alignment - Decisions ledger for echo-types ecosystem alignment

Architecture

┌─────────────────────────────────────────────────────────┐
│ Oblíbený Architecture │
├─────────────────────────────────────────────────────────┤
│ │
│ ┌──────────────┐ ┌──────────────┐ │
│ │ Factory Form │────────▶│ Constrained │ │
│ │ (Turing- │ emits │ Form │ │
│ │ complete) │ │ (Turing- │ │
│ │ │ │ incomplete) │ │
│ └──────────────┘ └──────┬───────┘ │
│ Compile-time │ Runtime │
│ Metaprogramming │ Execution │
│ ▼ │
│ ┌─────────────────┐ │
│ │ Accountability │ │
│ │ Trace │ │
│ │ (Immutable) │ │
│ └─────────────────┘ │
│ │
├─────────────────────────────────────────────────────────┤
│ Tooling Layer │
├─────────────────────────────────────────────────────────┤
│ Compiler │ Static Analyzer │ Debugger │ Profiler │
│ LSP │ VSCode Ext │ CLI │ Crypto FFI │
└─────────────────────────────────────────────────────────┘

Security Model

Turing-Incompleteness Guarantee

Oblibeny’s constrained form is intentionally Turing-incomplete:

1. Syntactic restrictions prevent unbounded computation

2. Call graph analysis ensures acyclicity

3. Static bounds checking verifies all loops terminate

4. Formal verification proves termination mathematically

This makes Oblibeny ideal for: - Hardware Security Modules (HSMs) - Secure enclaves (SGX, TrustZone) - Smart cards - Critical embedded systems - High-assurance cryptographic code

Post-Quantum Cryptography

Crypto stack via Zig FFI: - Dilithium5 - Lattice-based signature - SPHINCS+ - Hash-based signature - Kyber1024 - Lattice-based KEM - Ed25519 - Classical fallback

Libraries: liboqs 0.10.0+ and libsodium 1.0.19+

Project Statistics

Metric	Value
Lines of Code	~5,900 (OCaml 4,304 + Zig 1,047 + Idris2 554; measured 2026-06-12)
Files	170 tracked
Languages	OCaml (20 files), Zig (5 files), Idris2 (3 files)
Status	Active development (see .machine_readable/6a2/STATE.a2ml)
Test Coverage	27-test conformance suite, CI-gated (PR #52)
Documentation	Complete (spec + tutorial + examples)
Container Size	~50MB (minimal runtime)

Contributing

See CONTRIBUTING.adoc for development guidelines.

Code of Conduct: CODE_OF_CONDUCT.md

License

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

Oblíbený is free software under the Palimpsest License (MPL-2.0).

See LICENSE for full terms.

Related Projects

• Svalinn - Edge gateway for verified containers

• Vörðr - Formally verified container runtime

• Selur - Zero-copy WASM bridge

• Verified Container Spec - Formal specification

• NextGen Languages - Language portfolio

Contact

• Issues: https://github.com/hyperpolymath/oblibeny/issues

• Discussions: https://github.com/hyperpolymath/oblibeny/discussions

• Author: Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk>

---

Guardian of correctness. Keeper of accountability. Beloved for its guarantees. 🔐✨