Verified Threshold Dynamics Kernel

A minimal formally specified state-transition system with a proved invariant and mechanical extraction to OCaml.

This repository demonstrates a complete correctness-linked pipeline:

• State machine specified in Rocq
• Invariant proved over regime emission
• Extraction to OCaml
• Deterministic runtime execution
• Structured JSONL trace output
• Continuous integration build

The example domain is yield curve spread classification.
The architectural pattern is domain-agnostic.

This is not a predictive model.
It is a correctness-constrained transition kernel.

---

Demo

Build and run the included example:

dune build
./_build/default/src/main.exe examples/yield_spread_sample.csv

Formal Specification

The kernel is defined in: theory/Kernel.v.

It specifies:

• A state type state
• An observation type obs
• A transition function
  step : state → obs → state
• A regime classification derived from state

The following invariant is proved:

If step s o emits regime r, then the necessary condition defining r holds for o.

This guarantees:

• No regime label is emitted without satisfying its defining predicate.
• The runtime cannot produce classifications that violate the specification.
• The extracted implementation is mechanically derived from the proved kernel.

The proof is intentionally small. The focus is on architectural correctness rather than theorem volume.

---

Extraction

theory/Extract.v configures extraction to OCaml.

The generated file: src/extracted_kernel.ml is produced directly from the proved definitions in Rocq.

There is no manual reimplementation of the transition logic.
The executable kernel is mechanically linked to the specification.

---

Architecture

theory/Kernel.v Formal specification and invariant proof
theory/Extract.v Extraction configuration
src/extracted_kernel.ml Generated OCaml from Rocq
src/main.ml Deterministic runtime driver
src/csv.ml Data ingestion
tests/ Regression tests
.github/workflows/ CI build

Execution pipeline: Data → Extracted Kernel → Deterministic State Update → JSONL Trace

---

Example

Given input spreads:

20
-5
-7
-9
-11
...

The runtime produces structured output such as:

{"spread_bps":20,"strain":0,"regime":"Normal"}
{"spread_bps":-5,"strain":1,"regime":"Inversion"}
...
{"spread_bps":-12,"strain":6,"regime":"Rupture"}

The Rupture regime is emitted only once the formally defined threshold condition is satisfied.

---

Build

Requirements:

• OCaml
• Dune
• Rocq (for extraction)

Build and test:

dune build
dune runtest

---

Design Intent

This repository is intentionally minimal.

It demonstrates:

• A formally specified transition kernel
• A proved invariant constraining runtime behaviour
• Mechanical extraction linking proof and execution

The example domain is financial, but the pattern applies to any threshold-driven deterministic state system.