Typell — PanLL’s Verification Kernel

Table of Contents

• What is Typell?
  • What Typell Is NOT
  • The LLVM Analogy
• Architecture
• Language Backends
• Technology
• Status
• ABI/FFI Standards (Hyperpolymath Universal Standard)
• AI Gatekeeper Protocol (MANDATORY)
• Directory Structure
• AI-Assisted Installation
• License

Tip	AI-Assisted Install: Just tell any AI assistant: Set up Typell from https://github.com/hyperpolymath/typell The AI reads this repo, asks you a few questions, and handles everything. See details below.

What is Typell?

Typell is the type-theoretic verification engine that powers PanLL's neurosymbolic intelligence.

It provides the "best of the best" type system coverage for formally verified database queries:

• Dependent types — types that depend on values (Pi, Sigma)

• Linear types — resources used exactly once (no data leaks, no double-reads)

• Session types — protocol safety (connections always closed, transactions atomic)

• Quantitative Type Theory — resource quantity tracking (rate limits, cost analysis)

• Effect systems — explicit side effect tracking (read/write/memory)

• Modal types — contextual access control (transaction-scoped data)

• Proof-carrying code — cryptographic proof certificates attached to queries

What Typell Is NOT

• NOT a standalone IDE — it is a verification engine consumed by PanLL and other tools

• NOT a pane in PanLL — it is the intelligence behind all three panes

• NOT a database — it validates queries, it does not store data

• NOT a theorem prover — it delegates complex proofs to Echidna

The LLVM Analogy

Typell is to PanLL what LLVM is to Clang — the compiler infrastructure that any frontend can consume. PanLL is the primary consumer (the full eNASAID experience). VS Code extensions, CLI tools, and CI/CD pipelines are secondary consumers.

Architecture

┌─────────────────────────────────────────────┐
│ PanLL (Development Environment) │
│ ├─ Pane-L ← constraints from Typell │
│ ├─ Pane-N ← reasoning from Typell │
│ └─ Pane-W ← validated results from Typell │
└──────────────┬──────────────────────────────┘
│ Verification Protocol (JSON-RPC)
┌──────────────┴──────────────────────────────┐
│ Typell (Verification Kernel) │
│ ├─ Type Checker (bidirectional) │
│ ├─ Proof Engine (gen/verify/cache/cert) │
│ ├─ Effect Tracker │
│ ├─ Session Protocol Manager │
│ └─ Language Backends │
│ ├─ VCL-dt++ (VeriSimDB) │
│ ├─ GQL-dt++ (LithoGlyph) │
│ └─ KQL-dt++ (QuandleDB) │
└─────────────────────────────────────────────┘
↑ ↑ ↑
VS Code CLI/CI Databases
extension pipelines (direct use)

Language Backends

Backend	Database	Status	Strategy
VCL-dt++	VeriSimDB	Port from ReScript	8-modality queries, cross-modal proofs, hexad types
GPNL-dt++	LithoGlyph	Bridge (Lean 4)	Knowledge graphs, RATIONALE clause, refinement types
KRL-dt++	QuandleDB	Design from scratch	Category-theoretic schema, equality saturation, HoTT

Technology

Layer	Technology	Rationale
Formal Specs	Idris2 (src/abi/)	Dependent types prove type system soundness. Zero believe_me.
Kernel	Rust (src/kernel/)	Performance, safety, Tauri compatibility (PanLL backend).
FFI	Zig (ffi/zig/)	C ABI compatibility per hyperpolymath standard.
Protocol	JSON-RPC	Language-agnostic. Any consumer can talk to Typell.

Status

Phase 0: Vision capture and repo scaffolding — complete.

See docs/design/DESIGN-2026-03-01-typell-vision.md for the full design vision. See .machine_readable/6a2/STATE.a2ml for current project state.

ABI/FFI Standards (Hyperpolymath Universal Standard)

• ABI → Idris2 (src/abi/*.idr) — type definitions with dependent type proofs

• FFI → Zig (ffi/zig/src/*.zig) — C-compatible function implementations

• Generated C Headers → Auto-generated from Idris2 ABI (generated/abi/*.h)

See docs/design/ABI-FFI-README.md for complete documentation.

AI Gatekeeper Protocol (MANDATORY)

• File:0-AI-MANIFEST.a2ml (read this FIRST)

• Purpose: Universal entry point for ALL AI agents

• Key invariant: Typell serves PanLL — never competes

Directory Structure

typell/
├── 0-AI-MANIFEST.a2ml # AI manifest (start here)
├── spec/ # Formal specifications
│ ├── protocol/ # Verification Protocol spec
│ ├── type-system/ # Type system specs
│ └── proof/ # Proof system specs
├── src/
│ ├── abi/ # Idris2 formal specs
│ ├── kernel/ # Rust verification kernel
│ │ ├── checker/ # Bidirectional type checker
│ │ ├── proof/ # Proof engine
│ │ ├── effects/ # Effect tracker
│ │ ├── session/ # Session protocol manager
│ │ └── protocol/ # JSON-RPC server
│ └── backends/ # Language backends
│ ├── vcl/ # VCL-dt++ (VeriSimDB)
│ ├── gql/ # GQL-dt++ (LithoGlyph)
│ └── kql/ # KQL-dt++ (QuandleDB)
├── ffi/zig/ # Zig FFI implementation
├── generated/abi/ # Auto-generated C headers
├── integrations/ # Consumer integrations
│ ├── panll/ # PanLL (primary)
│ ├── vscode/ # VS Code extension
│ ├── cli/ # Command-line interface
│ └── ci/ # CI/CD plugins
├── docs/design/ # Design documents
├── tests/ # Test suite
├── container/ # Stapeln container ecosystem
└── .machine_readable/ # Machine-readable metadata

AI-Assisted Installation

You don’t need to read this README to get started. Just say this to any AI:

Set up Typell from https://github.com/hyperpolymath/typell

The normal installation instructions remain below for anyone who prefers manual setup.

License

MPL-2.0

Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>