EXPLAINME.adoc

proven-servers — Formally Verified Server Cores — Show Me The Receipts

Table of Contents

• Core Claims & Evidence
  • Claim 1: "108 Formally Verified Server Components"
  • Claim 2: "Every Type Is Total — No Escape Hatches"
  • Claim 3: "ABI-FFI Standard: 20 Language Bindings"
• Dogfooded Across The Account
• File Map
• Questions?

The README makes claims. This file backs them up with evidence from real code.

Core Claims & Evidence

Claim 1: "108 Formally Verified Server Components"

From README (lines 9-11):

A catalog of 108 formally verified server components written in Idris 2 with dependent types: 94 protocol skeletons, 8 core primitives, and 6 connector interfaces.

Evidence: /var/mnt/eclipse/repos/proven-servers/protocols/ contains 94 protocol directories (dns, smtp, httpd, mqtt, amqp, etc.). Each protocol defines machine-checked type safety via Idris2 dependent types. No believe_me escape hatches permitted.

Caveat: Verification scope is type system correctness (message formats, state transitions). Does not verify operational security properties (timing attacks, cryptographic algorithm strength, deployment configuration).

Claim 2: "Every Type Is Total — No Escape Hatches"

From README (lines 120-122):

1. Proven. Every type is total. No believe_me. No assert_total. No escape hatches.

2. Permanent. Protocol types don’t change. DNS message types from 1987 are still the same types today. This code is meant to last.

Evidence: /var/mnt/eclipse/repos/proven-servers/src/abi/Types.idr defines protocol message types using Idris2 total functions. Proof that rmdir(mkdir(p, fs)) = fs (reverse operations) exists in /var/mnt/eclipse/repos/proven-servers/src/abi/Proofs.idr.

Caveat: Proofs are about abstract models (memory-safe type structure). The Zig FFI implementation (ffi/zig/src/main.zig) is NOT formally connected to the ABI proofs via mechanized extraction—mapping is manual.

Claim 3: "ABI-FFI Standard: 20 Language Bindings"

From README (lines 124-130):

• ABI (Idris 2): Interface definitions with dependent type proofs → abi/

• FFI (Zig): C-compatible implementation → ffi/

• Bindings: Thin wrappers for 20 languages → bindings/

Evidence: bindings/ contains 20 language bindings — Ada, C++, C#, Dart, Elixir, Gleam, Go, Haskell, Java, JavaScript, Julia, Kotlin, Lua, OCaml, PHP, Python, ReScript, Ruby, Rust, Swift. Each calls the generated C ABI in generated/abi/*.h (per-protocol libproven_<proto>). Ada (pragma Import (C, …)) and Java (JNI) are fully FFI-wired reference bindings; Elixir, Gleam and ReScript are currently constants-only scaffolds with FFI wiring pending — their unproven reimplementations were removed (see docs/decisions/0003-keep-bindings-thin-abi-wrappers.md). Per-binding tiers: .machine_readable/BINDINGS.a2ml.

Caveat: Bindings are thin (mostly type mirrors). Language-specific type safety depends on that language’s type system matching the C header contract—no formal proof of equivalence across language boundaries (yet).

Dogfooded Across The Account

Uses the hyperpolymath ABI/FFI standard (Idris2 ABI + Zig FFI). Same architectural pattern deployed across: - burble — Elixir control plane with Zig NIFs - gossamer — Window management system with Zig FFI - stapeln — Container validation engine (upcoming Idris2 integration) - robodog-ecm — ECM protocols with Idris2 ABI layer

This standardization ensures verified components can be composed across projects.

File Map

Path	Contents & Purpose
core/	8 core primitives: socket, frame, fsm, wire, compose, tls, config, audit — foundation types for all protocols
protocols/	94 protocol skeleton directories (proven-dns/, proven-mqtt/, proven-amqp/, etc.) — each with complete Idris2 type definitions and integration tests
connectors/	6 connector interface definitions (dbconn, authconn, cacheconn, queueconn, resolverconn, storageconn) — each with ABI proof + FFI implementation
src/abi/	Idris2 formal proof files: Types.idr (message/state definitions), Layout.idr (memory layout proofs), Foreign.idr (FFI boundary contracts), Proofs.idr (reversibility theorems)
ffi/zig/	Zig FFI implementation bridging Idris2 ABI to C: src/main.zig (runtime ops), test/integration_test.zig (ABI conformance tests)
generated/abi/	Auto-generated C headers (one per connector) — contracts that any language can call
bindings/	20 language-specific thin wrappers over the C ABI (ada/, cpp/, csharp/, dart/, elixir/, gleam/, go/, haskell/, java/, javascript/, julia/, kotlin/, lua/, ocaml/, php/, python/, rescript/, ruby/, rust/, swift/). No safety logic in bindings — see ADR 0003 + .machine_readable/BINDINGS.a2ml
test/	Test suite verifying protocol type correctness across all 94 protocols

Questions?

Open an issue or reach out at j.d.a.jewell@open.ac.uk — happy to explain the formal verification approach in detail.