NF-Sketches Formal Lab

The Formal Truth Layer. Absolute structural certainty requires mathematical rigor. NF-Sketches is our companion formal lab built entirely in the Lean 4 Theorem Prover, acting as the independent mathematical bedrock for the Monist Engine.

View GitHub Repository

1. The Dual-Verification Pipeline

Structural certainty requires mathematical rigor. Monist features a fully synchronized Differential Equivalence Testing pipeline that links the high-speed Rust evaluator to a formal, machine-checked embedding in Lean 4.

When a geometric compilation occurs, the core engine exports an SMT-LIB witness explicitly capturing the graph’s evaluation limits. The Lean interpreter ingests this block via an independent Bellman-Ford implementation to trace the identical constraints, mathematically proving that bare-metal execution matches machine-checked soundness.

2. The SMT-LIB Bridge

The system automatically pipes these SMT-LIB blocks into the Lean 4 parse-strat interpreter.

Inside Lean 4, an entirely independent topological Bellman-Ford pass traces the exact SMT constraints generated by the Rust compiler. This cross-language architecture mathematically proves that the exact execution topology used for hardware compilation strictly obeys Quine’s relative type-shifting bounds without scope leakage.

3. Structural Proofs and Boundaries

Our Lean 4 repository formalizes the mechanical limits of typestate extraction across our core formal validation environments: nf-validate and seq-embed. Key formalizations include:

  • StratificationSoundness.lean: Proving that resolving localized constraint graphs satisfies Quine’s rigid type-shifting limits.
  • BellmanFordInvariants.lean: Mathematically verifying that negative-weight cycle detection correctly identifies non-normalizable proofs (e.g., Russell’s Paradox and Specker’s Refutation bounds).
  • T-Relative Adjunctions: Utilizing Rosser’s Axiom of Counting to process \(+2\) typestate elevations in \(O(1)\) time without memory explosion.

By establishing a 1-to-1 equivalence between the Rust physical evaluator and the Lean geometric verifier, First Synthesis guarantees that only structurally verified, paradox-free Directed Acyclic Graphs reach the GPU.