Quintessence

Verification for the part of Elixir/OTP that can carry a proof.

Repository description: Three-layer formal verification suite for Elixir/OTP/BEAM: sequential pure subsets with TINI + MPR R5 non-interference, choreographic K-CUT GenServer protocols, and Idris2 QTT ABI + verified Zig NIFs under MaxPlus 1 ms scheduler bounds, backed by Z3, CVC5, Alethe proof checking, and ECHIDNA mutation gates.

Topics (20): hyperpolymath · open-source · epistemic-computing · epistemic-infrastructure · equivalence-aware-computing · typed-provenance · veridical-computing · formal-verification · elixir · beam · otp · zig · idris2 · smt-solving · proof-certificates · choreographic-programming · session-types · noninterference · max-plus-algebra · maximum-principal-reduction

Quintessence is a three-layer formal verification suite for Elixir/OTP. It proves three properties the standard BEAM toolchain does not:

1. Layer A (Sequential subset) — pure functions satisfy their @pre/@post contracts for all valid inputs, terminate along an explicit @measure, and preserve secret-types lattice TINI non-interference.

2. Layer B (OTP / GenServer protocol layer) — processes claim remote state commitment only across proved two-party K-REPLY causal round-trips (choreographic-types Y-6/Y-8), never across asynchronous cast/send, under bounded mailbox occupancy and supervision epoch restarts (k = 12 BMC).

3. Layer C (Native NIF boundary) — Zig/Rustler NIFs satisfy C1—​C12 safety obligations, match their reproducible binary SHA-256 receipt at load time, and satisfy MaxPlus ⇐ 1,000 us for normal BEAM schedulers (or declare schedule: :dirty_cpu).

Important

Current implementation state (v0.1.0-alpha vertical slice): The native Zig compiler/verifier (src/core/ + src/interface/ffi/), dual Z3 5.3.1 + CVC5 1.4.2 SMT & Alethe proof-DAG kernel checker, k = 12 symbolic BMC engine, Layer C MaxPlus / dlopen / SHA-256 receipt verifier, 6-kind ECHIDNA mutation engine, Elixir Mix frontend (mix.exs, lib/), and 15-case live regression suite (tests/quintessence/run_suite.sh) compile and execute today, producing honest TrustLevel 4 local certificates. Batch coqc + lean TrustLevel 5 promotion and beam_lib bytecode tracing are scheduled in Milestones M1—​M5 of the Implementation Plan.

Contents

• The pipeline
• What exists in this repository
• Quick start
• AI-Assisted Installation
• Licence
• Provenance

The pipeline

Elixir source
  |  G0  deterministic macro & purity firewall (`Q-101`..`Q-108`, `Q-206`)
  v
  |  G1  subset checker + Face elaborator
  v
Core Spec IR  (`qir/v1`, RFC 8785 JCS content-addressed, Idris2 QTT model)
  |------------------+-------------------+-------------------+
  v                  v                   v
Layer A            Layer B             Layer C
QF_UFLIA / QF_BV   K-CUT + k=12 BMC    Idris2 ABI / Zig C1-C12 / MaxPlus
  |                  |                   |
  +---------+--------+---------+---------+
            v
   Z3 + CVC5 + Native Alethe Proof-DAG Kernel  ->  6-Kind Mutation (>= 95%)
            v
   TrustLevel 4 Warrant/Receipt  ->  batch Coq + Lean  ->  Level 5 Receipt

What exists in this repository

Path	Contents
Implementation Plan	Engineering execution blueprint, v0.1.0-alpha reality audit, pass-by-pass design, empirical solver/ELF findings, and Milestones M1—​M5 to v1.0.0.
Architecture	Full architectural specification: pipeline, qir/v1, Layers A/B/C, evidence, mix verify, risks, traceability, foundations, and error catalogue.
Layer A	Sequential subset grammar, refinements, typing rules, Why3/SMT projection, TINI non-interference, and G0a—​G0c firewall.
Layer B	Proved two-party fragment, GenServer Face, K-CUT-LOSS/WARRANT, K-REPLY, mailbox high-water-mark calculus, supervision epochs, and TLA+ model.
Layer C	Idris2 QTT ABI, Rustler rules, alloc-free Zig core, C1—​C12 receipt schema, and tropical MaxPlus BEAM scheduler timeslice law.
Evidence	Warrant/Receipt JCS schemas, trust ladder, ECHIDNA dispatch, Alethe/Dedukti certificates, vacuity V1—​V5, and 6-kind mutation scoring.
Roadmap	Phased roadmap (Phases 0—​6), WP-01..WP-27 work breakdown, gates, and metrics.
src/core/, src/interface/	Native Zig 0.17 verifier engine (quintessence CLI + libquintessence.so) and %default total Idris2 QTT ABI (src/interface/Abi/Qir.idr).
mix.exs, lib/	Elixir package (Quintessence, Quintessence.Face, Quintessence.Nif, Quintessence.Tracer, and mix verify / doctor / explain / receipt).
Worked example	Verisim.Spec, Verisim.Entity, Verisim.Nif, verisim_nif.zig, JCS NIF receipt, Idris2 model, and TLA+ protocol model — verified end to end (12 QEDs, 25,910 Alethe steps, 100.00% mutation score).

Architectural rationale is recorded in ADR-0004.

Quick start

just build                                                       # build libquintessence.so + CLI
./src/interface/ffi/zig-out/bin/quintessence doctor              # check Z3, CVC5, Zig, Alethe kernel
./src/interface/ffi/zig-out/bin/quintessence verify examples/quintessence
just test                                                        # 10 Zig unit tests + 15 E2E cases
just validate                                                    # RSR structure, deed, AI guide

When Elixir/Mix is installed alongside the native binary:

mix quintessence.doctor
mix verify examples/quintessence --strict
mix quintessence.explain Q-401

AI-Assisted Installation

For AI agents working in or extending this repository: read quintessence_chora.deed, CLAUDE.md, and docs/status/ROADMAP.adoc first, then follow docs/AI_INSTALLATION_GUIDE.adoc and docs/architecture/REPOSITORY-MAP.adoc.

Licence

Code is Mozilla Public License 2.0 (MPL-2.0); documentation and prose are CC-BY-SA-4.0. Every file carries an explicit SPDX-License-Identifier header.

Provenance

Minted from hyperpolymath/rsr-template-repo under RSR canon v2.1.2 (fv clade: Formal Verification & Proofs). Builds on the estate’s upstream foundations (choreographic-types, secret-types, epistemic-types, tropical-types, occupancy-types, and echidna).