Snapkitty/xrex-invariants-formal

XREX Invariants Formal

Formal Verification of Computational Kernel Behavior

Execution is evidence. Proof is certainty.

XREX Invariants Formal moves the project from implementation into mathematical proof.

The repository contains formal verification artifacts that express, check, and prove properties about computational kernel behavior.

The central question:

Does the implementation preserve the property that the specification says must remain invariant?

---

The Problem

A program can execute successfully and still be wrong.

SPECIFICATION
    says: "property P must hold"

IMPLEMENTATION
    runs: "exit code 0"

QUESTION
    did property P actually hold?

A successful execution is evidence.

It is not proof.

XREX Invariants treats correctness as a mathematical object rather than simply a successful program exit.

---

Architecture

SPECIFICATION
     ↓
INVARIANT (mathematical property)
     ↓
FORMAL PROOF (Agda / Lean)
     ↓
IMPLEMENTATION (Haskell / Scala)
     ↓
BUILD-TIME CHECK (Starlark)
     ↓
RUNTIME VERIFICATION

Each layer answers a different question:

Layer	Question
Specification	What should be true?
Invariant	What must not change?
Proof	Is the invariant actually preserved?
Implementation	Does the code match the specification?
Build-time check	Is the invariant enforced during compilation?
Runtime	Is the property holding right now?

---

Components

File	Language	Purpose
Core.agda	Agda	Formal proof of XREX kernel invariants
PhoenixInvariants.scala	Scala	Executable invariant checks
phoenix_invariants.star	Starlark	Build-time invariant enforcement
dreamcycles/	Haskell	Dreamcycles invariant research

---

The Invariant

An invariant is a property that must remain true across all valid transformations of the system.

STATE₀  →  TRANSFORM  →  STATE₁

INVARIANT(STATE₀) = true
INVARIANT(STATE₁) = true

For ALL valid transformations.
Not just the ones we tested.

Testing checks specific inputs.

Proof checks all possible inputs.

That distinction is the entire contribution of formal methods.

---

Agda Layer

Agda is a dependently-typed proof assistant.

The Core.agda file expresses the XREX kernel invariants as types.

In Agda, a type that is inhabited (has a value) is a theorem that has been proven.

TYPE          →  THEOREM
INHABITANT    →  PROOF
TYPE-CHECKING →  VERIFICATION

If the file type-checks, the invariants are proven.

If it does not type-check, the invariants are not proven.

There is no middle ground.

---

Scala Layer

The Scala implementation provides executable invariant checks.

These are not proofs.

They are runtime monitors that can detect invariant violations during execution.

EXECUTION
    ↓
OBSERVATION
    ↓
INVARIANT CHECK
    ↓
PASS / VIOLATION

The Scala layer answers: "Is the invariant holding right now?"

The Agda layer answers: "Must the invariant hold always?"

Both questions matter.

---

Starlark Layer

Starlark provides build-time enforcement.

Before code is compiled, the invariant constraints are checked against the build configuration.

BUILD REQUEST
    ↓
STARLARK RULES
    ↓
INVARIANT GATE
    ↓
COMPILE / REJECT

This prevents code that violates structural invariants from being built at all.

---

Haskell Layer (Dreamcycles)

The Dreamcycles project explores invariants in functional computation.

Haskell's type system provides a middle ground between Agda's full dependent types and Scala's runtime checks.

AGDA     →  full proof (dependent types)
HASKELL  →  partial proof (parametric types + laws)
SCALA    →  runtime check (assertions)
STARLARK →  build-time check (structural rules)

Each level provides a different strength of guarantee at a different cost.

---

Research Philosophy

Correctness is not binary at the system level

A kernel can be:

• type-correct but semantically wrong
• semantically correct but numerically unstable
• numerically stable but violating a higher-level invariant
• invariant-preserving but not the invariant you intended

Formal methods make these distinctions explicit.

Proof is expensive but permanent

Writing a proof takes more effort than writing a test.

But a proof covers all cases.

A test covers the cases you thought of.

The invariant outlives the implementation

Implementations change.

If the invariant is expressed independently, it survives those changes.

If the invariant is embedded in the implementation, it dies with the implementation.

XREX keeps them separate.

---

Getting Started

git clone https://github.com/SNAPKITTYWEST/xrex-invariants-formal.git
cd xrex-invariants-formal

# Type-check Agda proofs (requires Agda 2.6+)
agda Core.agda

# Run Haskell invariant suite
cd dreamcycles
cabal test

# Check Scala invariants
scala PhoenixInvariants.scala

---

Status

Research / Experimental

The formal artifacts represent verified properties about kernel behavior.

Not all implementation code has been fully verified against all formal specifications.

The architecture for connecting proof to implementation is the primary contribution.

---

Copyright

Copyright BEL ESPRIT D ACCORD TRUST HOLDINGS INC.

See LICENSE for the governing terms.

---

execution is evidence.
proof is certainty.
the invariant outlives the implementation.
own the correctness.