Vext: Verifiable, Extensible Communications Protocol

Table of Contents

• Overview
  • The Problem
  • The Solution
• Architecture
  • Three Layers
  • a2ml: Anti-Algorithm Markup Language
  • Protocol Bridges
• Use Cases
  • For Journalists
  • For Privacy Advocates
  • For Everyone
• Research
  • arXiv Paper (Planned)
  • NUJ Discussion Paper
• Implementation Status
• Documentation
• Quick Start
• Contributing
• License
• Contact
• Acknowledgments

Overview

Vext is a cryptographically verifiable communications protocol that provides mathematical proof of algorithmic neutrality. It combines proven protocols (NNTP, Email, Gemini) with modern cryptographic guarantees (Merkle trees, digital signatures, formal verification).

Key Innovation: The a2ml (Anti-Algorithm Markup Language) verification layer, which requires Idris2’s dependent types to provide compile-time proofs of feed integrity.

The Problem

Modern social media platforms:

• ❌ Use opaque algorithms to reorder, filter, and inject content

• ❌ Insert advertisements disguised as organic content

• ❌ Shadowban users without transparency

• ❌ Profile users for targeted manipulation

• ❌ Cannot prove they don’t manipulate feeds

Result: Information asymmetry, manipulation, broken economics for creators.

The Solution

Vext provides cryptographic proofs that feeds are:

• ✅ Chronological (not algorithmically sorted)

• ✅ Ad-free (no injected advertisements)

• ✅ Uncensored (no hidden messages)

• ✅ Verifiable (users can check the math)

Don’t trust us. Verify the cryptography.

Architecture

Three Layers

┌──────────────────────────────────┐
│  a2ml Verification Layer         │  ← NEW (Idris2, dependent types)
│  (Cryptographic proofs)          │
├──────────────────────────────────┤
│  NNTPS Transport Layer           │  ← EXISTING (40+ years proven)
│  (Flooding, distribution)        │
├──────────────────────────────────┤
│  TCP/IP + TLS                    │
└──────────────────────────────────┘

a2ml: Anti-Algorithm Markup Language

Why Idris2?

a2ml requires dependent types to prove properties at compile-time:

• Type-level proofs that feeds are chronological

• Totality checking (proofs cannot loop infinitely)

• Linear types (resources consumed exactly once)

• Formal verification exceeding what ATS, Rust, or Coq can provide

Example (Idris2):

-- Chronological feed proven at TYPE LEVEL
data ChronologicalFeed : List Message -> Type where
  Empty : ChronologicalFeed []
  Cons : (m1 : Message) -> (m2 : Message) ->
         {auto prf : timestamp m1 <= timestamp m2} ->
         ChronologicalFeed (m2 :: rest) ->
         ChronologicalFeed (m1 :: m2 :: rest)

-- IMPOSSIBLE to construct if feed isn't chronological!

This is impossible in Rust, Go, or even ATS.

Protocol Bridges

Vext connects to existing protocols:

Protocol	Use Case	Status
NNTP	Newsgroups, power users	Core protocol
Email	Universal access, mailing lists	Gateway implemented
SMS	Mobile access (basic)	Planned
RCS	Mobile access (rich)	Planned
Gemini	Smol internet, privacy	Planned
Matrix	Federation bridge	High priority
Web	Universal fallback	PWA planned

Use Cases

For Journalists

• Attribution guaranteed (cryptographic signatures)

• No censorship (provably uncensored feeds)

• Source protection (E2E encryption for DMs)

• Fair compensation (direct support, no platform tax)

For Privacy Advocates

• No profiling (no algorithmic targeting possible)

• No tracking (DIDs instead of emails/phone numbers)

• Open source (reproducible builds)

• Formal verification (proven secure)

For Everyone

• Chronological feeds (like "the old internet")

• No ads (cryptographically proven)

• No manipulation (mathematically impossible)

• Works everywhere (email, SMS, web, native apps)

Research

arXiv Paper (Planned)

Title: Cryptographic Proofs of Algorithmic Neutrality in Federated Communication Systems

Categories: * cs.CR (Cryptography and Security) - Primary * cs.NI (Networking and Internet Architecture) * cs.CY (Computers and Society)

Status: Implementation in progress, paper draft planned for Q2 2025

See: arXiv Paper Plan

NUJ Discussion Paper

For: National Union of Journalists Ethics Council

Framing: Labor and ethics issue, not just technology: * Platform dependency hurts journalists * AI pollution undermines attribution * Broken economics (platform takes 30-50% cut) * Censorship without accountability

See: NUJ Proposal

Implementation Status

Component	Language	Status
a2ml specification	Idris2	Design phase
a2ml verification library	Idris2	Not started
NNTP integration	Rust	Planned
Email gateway	Rust	Prototype complete
SMS/RCS gateway	Rust	Planned
Matrix bridge	Rust	Planned
Reference client	Rust/Idris2	Not started
Formal verification	Idris2/Kani	Design phase

Documentation

• Manifesto - Why vext exists

• Technical Specification - Protocol details

• a2ml Architecture - Cryptographic design

• Multicast Architecture - Tag-based distribution

• Mobile Strategy - SMS/RCS/Email gateways

• Protocol Bridges - Matrix, Nostr, etc.

• arXiv Paper Plan - Research publication plan

• Roadmap - Implementation timeline

Quick Start

# Clone repository
git clone https://github.com/hyperpolymath/vext
cd vext

# Install Idris2 (required for a2ml)
# See: https://idris-lang.org/pages/download.html

# Build a2ml specification (when available)
cd a2ml-spec
idris2 --build

# Run tests
idris2 --test

Contributing

This is research-stage software. Contributions welcome, especially:

• Idris2 experts (a2ml specification)

• Cryptography experts (security review)

• NNTP experts (protocol integration)

• Formal verification experts (Idris2 proofs)

See: Contributing Guidelines

License

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

Copyright (c) 2025 Jonathan D.A. Jewell

See: Full License Text

Contact

• Author: Jonathan D.A. Jewell

• Email: jonathan.jewell@open.ac.uk

• GitHub: https://github.com/hyperpolymath/vext

• Matrix: (coming soon)

Acknowledgments

• NUJ (National Union of Journalists) - Labor perspective

• NNTP community - 40+ years of proven protocol design

• Idris2 community - Dependent types and formal verification

• Journalists, activists, privacy advocates - Motivation and use cases

---

"Don’t trust us. Verify the math."