NMLT

NMLT - New Mathematics, Languages, and Techniques is a research repository investigating candidate mathematical foundations, developing formal languages, and testing evidence-directed techniques.

Comment

Inspiration

When OpenAI gave me another weekly rate-limit reset, I was inspired to make every single token count. NMLT was the most impactful project I could think of—the absolute best use of that capability.

Looking at today's AI landscape, I could see that tools like TLA+ and existing formal languages held enormous potential, but standard frameworks were never built for the age of autonomous agentic fleets. To make superintelligent systems a reality, we couldn't just patch legacy tools or rely on probabilistic guessing. We needed an ambitious attempt to create methods and systems that go far beyond current capabilities.

That conviction gave birth to NMLT (Nova Mathematica · Linguae · Technicae). It is driven by a simple, uncompromising thesis: To truly progress, humanity needs new mathematics, new languages, and new techniques. NMLT is our attempt to build that behavior-first, evidence-carrying foundation—turning raw AI generation into provably trustworthy computation.

What it does

NMLT runs as an end-to-end research laboratory and verification engine for trustworthy computation.

The repository currently includes: a lossless parser, recovering syntax tree, formatter, resolver, typed HIR, explicit core, and command-line interface; deterministic finite-state model checking with reproducible witnesses; temporal, fairness, stuttering, hiding, refinement, and runtime-journal experiments; evidence artifacts bound to exact sources, tools, limits, and certificates; independent checking paths that reject stale, forged, or mismatched results; open-system composition with assumptions, guarantees, synchronous wiring, affine capabilities, resources, grades, and invariant transport; a bounded dependency-free Rust validation kernel translated to Lean with pinned Charon/Aeneas, plus shared positive and adversarial controls; and comparison models in TLA+, Quint, and P.

How we built it

This project was brought to life through a direct pair-programming partnership between me (Ian Carlos Fabin) and Sol (GPT-5.6 operating inside the OpenAI Codex CLI). Equipped with only my MSI Katana laptop, the core NMLT thesis, and a vision for verifiable AI, we set out to build an end-to-end laboratory for trustworthy computation.

I fed Sol as much architectural context, mathematical domain knowledge, and behavioral constraints as possible. Together, we crafted a step-by-step execution plan and drove the system to build the entire platform from scratch:

  1. Lossless Compiler & Core Engine (crates/nmlt-core, nmlt-engine, nmlt-cli): We prompted Sol in Codex CLI to construct an RFC-compliant CST lexer/parser, typed HIR resolver, explicit core calculus, and a deterministic finite-state BFS model checker with reproducible counterexample witnesses.
  2. Lean 4 Metatheory Pipeline: We designed crates/nmlt-open-kernel, a dependency-free Rust validation kernel. Using pinned Charon and Aeneas, we extracted Rust execution paths directly into Lean 4 metatheory (NMLT/Behavior/OpenKernelGenerated/) and proved mechanized zero-trust theorems (untrusted_cannot_execute, leader_requires_quorum_proof) in TrustHarness.lean.
  3. Multi-Engine Evidence Verification Suite: Sol generated cross-verified formal models in TLA+, Quint, and P, alongside Python verification readback scripts and JSON Schema evidence validators.

With nothing more than an MSI Katana laptop and the power of GPT-5.6 inside Codex CLI, we transformed a theoretical mathematical thesis into a fully verified, runnable formal language environment.

Challenges we ran into

  • Lean 4 Metatheory Equivalence: Bridging Aeneas-generated Rust structural equality to native Lean 4 inductive types required proving layer by layer that structural equality implies native Lean equality (EqualitySoundness.grade) without relying on unverified axioms.
  • Finite State Exploration Bounds: Ensuring state-space exploration over unbounded loop transitions remained strictly finite required designing discrete state bounds ($N \le 20$) without sacrificing behavioral verification rigor.
  • Contract-Sound Refinement Parity: Maintaining exact semantic refinement definitions across 4 distinct formal systems (NMLT, TLA+, Quint, and P) required rigorous label-aware transition mapping.

Accomplishments that we're proud of

  • Mechanized Lean 4 Proof Extraction: Successfully extracted Rust kernel execution paths to Lean 4 via Charon/Aeneas and proved zero-trust access control theorems (TrustHarness.lean), guaranteeing untrusted agent drafts can never execute without quorum proof grants.
  • Unified Master CI Pipeline (make ci): Achieved 100% clean passing tests across Rust workspace crates, Lean 4 theorem builds, Python evidence readback scripts, TLC (TLA+), and P model checkers under a single byte-identical Linux verification gate.
  • Honest Evidence Boundaries: NMLT is intentionally honest about verification limits—reporting bounded model checking as model_checked evidence and unproven claims as unknown, never making false claims.

What we learned

  • New Mathematics Potential: Studying classic formal specification systems like TLA+ alongside modern mathematics proved that combining foundational verification principles with new math yields unexpectedly powerful combinations for AI reliability.
  • Agentic Metatheory Co-Synthesis: GPT-5.6 inside Codex CLI excels at multi-language formal proof synthesis, seamlessly orchestrating Rust systems programming, Lean 4 theorem proving, and TLA+ model checking.
  • Evidence-Carrying Architecture: Bounded model checking with source-bound witness manifests provides a vastly stronger, reproducible safety guarantee for LLM code generation than standard unit testing alone.

What's next for NMLT

NMLT is pre-alpha research. Future research milestones include:

  • Expanding Lean 4 mechanized proofs from structural kernel equality to general source-to-certificate compilation.
  • Integrating NMLT real-time model checking into live LLM agent loop middleware (such as Codex CLI plugins).
  • Extending open-system rely/guarantee composition to infinite-state distributed actor networks.

Built With

Share this project:

Updates