Index
Documentation
The VSEL documentation set is structured as a dependency graph: semantics → invariants → constraints → proofs → audit evidence. Read in order when building, and use the navigation tree as a checklist for coverage and traceability.
Getting Started
Entry points: narrative framing, threat assumptions, and implementation boundaries.
04 docs
Verifiable Semantic Execution Layer (VSEL)
Modern cryptographic execution systems, particularly those leveraging zero-knowledge proofs, provide strong guarantees about the correctness of computation relative to a circuit. However, they fail to guarantee correctness relative to the intended semantics of the system they represent. This gap between *verified execution* and *correct execution* introduces systemic risk in financial, cryptographic, and distributed systems.
Tech Spec
**Verifiable Semantic Execution Layer (VSEL)**
Roadmap
**Verifiable Semantic Execution Layer (VSEL)**
Threat Model
**Verifiable Semantic Execution Layer (VSEL)**
Specification & Semantics
Formal models: state transitions, traces, semantic mapping, and preservation constraints.
08 docs
Formal Specification
**Verifiable Semantic Execution Layer (VSEL)**
State Machine
**Verifiable Semantic Execution Layer (VSEL)**
Transition Partitioning
**Verifiable Semantic Execution Layer (VSEL)**
Execution Trace Model
**Verifiable Semantic Execution Layer (VSEL)**
Trace Sufficiency
**Verifiable Semantic Execution Layer (VSEL)**
Semantic Mapping
**Verifiable Semantic Execution Layer (VSEL)**
Semantic Preservation Theorems
**Verifiable Semantic Execution Layer (VSEL)**
Semantic Gap Analysis — VSEL Refinement Chain
This document presents a systematic analysis of every semantic gap between the VSEL Lean 4 formal specification and the Rust implementation. The refinement chain R01 to R12 to R23 to R34 connects Lean 4 proofs to executable Rust code through a series of abstraction layers, each introducing axioms and opaque types that represent unverified trust assumptions. Every axiom is a point where the formal proofs assume something about the Rust code that has not been mechanically verified.
Constraints & Invariants
Invariant catalogs and constraint derivation artifacts. Source-of-truth for what must be enforced.
07 docs
Invariants
**Verifiable Semantic Execution Layer (VSEL)**
Economic Invariants
**Verifiable Semantic Execution Layer (VSEL)**
Constraint Derivation
**Verifiable Semantic Execution Layer (VSEL)**
Constraint Coverage Matrix
**Verifiable Semantic Execution Layer (VSEL)**
Underconstraint Analysis
**Verifiable Semantic Execution Layer (VSEL)**
Counterexample Catalog
**Verifiable Semantic Execution Layer (VSEL)**
Edge Case Atlas
**Verifiable Semantic Execution Layer (VSEL)**
Proof System
Proof/verification architecture, ZK backend integration, and non-malleability requirements.
09 docs
Proof Layer
**Verifiable Semantic Execution Layer (VSEL)**
Verification Layer
**Verifiable Semantic Execution Layer (VSEL)**
Proof Obligations
**Verifiable Semantic Execution Layer (VSEL)**
Witness Uniqueness and Non-Malleability
**Verifiable Semantic Execution Layer (VSEL)**
Invalid Execution Witness Suite
**Verifiable Semantic Execution Layer (VSEL)**
ZK Backend Integration Plan
This document defines the interface contract, component boundaries, and migration
Plonky3 Version Pinning and Security Analysis
| Repository | `https://github.com/Plonky3/Plonky3.git` |
Poseidon Parameter Justification
This document provides a comprehensive security analysis and justification for the
Goldilocks `reduce128` Cross-Reference Analysis
**Document**: `GOLDILOCKS_CROSS_REFERENCE.md`
Assurance & Audit
Composition, refinement, audit evidence, and long-term cryptographic posture.
11 docs
Composition Model
**Verifiable Semantic Execution Layer (VSEL)**
Assume-Guarantee Composition Model
**Verifiable Semantic Execution Layer (VSEL)**
Refinement Strategy
**Verifiable Semantic Execution Layer (VSEL)**
Model Checking Plan
**Verifiable Semantic Execution Layer (VSEL)**
Theorem Proving Plan
**Verifiable Semantic Execution Layer (VSEL)**
Audit Evidence Model
**Verifiable Semantic Execution Layer (VSEL)**
Self Audit
**Verifiable Semantic Execution Layer (VSEL)**
Axiom & Opaque Type Catalog — VSEL Refinement Chain
This document catalogs every `axiom` declaration and every `opaque` type/function
Axiom Validation Map
This document maps **every** axiomatized Lean 4 declaration in the VSEL formal specification to the Rust property-based tests that empirically validate it, the number of test cases executed, the boundary coverage achieved, and the residual risk assessment.
Cryptographic Model
**Verifiable Semantic Execution Layer (VSEL)**
Long-Term Security Model
**Verifiable Semantic Execution Layer (VSEL)**