Skip to content
JANUS DOCS

Compiler Determinism Proofs

Compiler Determinism Proofs

Section titled “Compiler Determinism Proofs”

Same source code. Same binary. Every time. Proved.

The Janus language claims determinism as one of its eight providence axes. That claim is now backed by machine-checked proofs.

In August 2026, a dedicated sprint produced Lean 4 formal models and proofs for seven core compiler algorithms. The proofs establish that the compiler’s design is sound — deterministic, confluent, and terminating — at the algorithmic level.

This is not a marketing claim. It’s a lake build that passes.

What Was Proved

Section titled “What Was Proved”
PriorityCompiler ComponentPropertyProof
P1Type Inference / UnificationConfluence, termination, correctnesssolve_deterministic_same_order (rfl), substitution_monotonic (unfold;simp)
P2QTJIR LoweringDeterminism, structural equivalencelowerUnit_deterministic (rfl), lowering_structural (congrArg)
P3SSA ConstructionDeterminismssa_deterministic (rfl)
P4Effect InferenceUnique fixpoint, monotonicity, order-independenceeffect_unique_fixpoint (rfl)
P5MonomorphizationIdempotence, key consistencymonomorph_idempotent (simp), monomorph_key_consistent (rw)
P6Call Graph ConstructionDeterminism, resolution stabilitycallgraph_deterministic (rfl)
P7Pipeline CompositionEnd-to-end determinismjanus_pipeline_deterministic (rfl)

The capstone theorem: parse → desugar → lower → SSA → transforms → emit → LLVM IR — the full pipeline is deterministic. If each stage is a pure function, the composition is a pure function. Same source code always produces the same binary.

How It Works

Section titled “How It Works”

Model-Based Verification

Section titled “Model-Based Verification”

The proofs use a model-based approach, a standard formal-methods pattern:

  1. Model the algorithm in Lean 4 as a pure functional specification
  2. Prove properties about the model (determinism, confluence, termination)
  3. Document the refinement mapping connecting the model to the Zig implementation

This is the same approach used by seL4 (Haskell model → C refinement), CompCert (Coq specification → OCaml extraction), and AWS s2n (Cryptol specs → C implementations).

The Models

Section titled “The Models”

Each algorithm is modeled as a mathematical function with no hidden state, no random seeds, and no environmental dependencies:

  • Type Unification: An 8-constraint-kind worklist solver, modeled as a purely functional fixed-point iteration over constraints and substitutions
  • QTJIR Lowering: A mutual-recursive expression-to-IR-graph translator covering 10 expression kinds across 5 representative lowering leaves
  • SSA Construction: A dominator-tree pipeline (dominators → dominance frontier → phi placement → renaming)
  • Effect Inference: A lattice-theoretic fixed-point propagation over a finite effect set
  • Monomorphization: An association-list cache with idempotent key→name mangling
  • Call Graph: A multi-unit ASTDB traversal with import-filtered callee resolution
  • Pipeline Composition: A 6-stage pipeline where each stage is a typed pure function

Why Determinism Matters

Section titled “Why Determinism Matters”

The deterministic axis (Axis Bit 1 in SPEC-100) means: given the same declared inputs, compiler version, target, manifest, capabilities, and dependency CIDs, this computation can be replayed with the same result.

This matters for:

  • Reproducible builds: Two developers on different machines compile to the same binary
  • Supply-chain verification: A reviewer can rebuild from source and get a byte-identical artifact
  • Auditability: The compiler doesn’t introduce nondeterminism through its own algorithms
  • Replay debugging: A program trace can be replayed exactly because the compiler didn’t add entropy

Repository

Section titled “Repository”

The proofs live in a separate repository at janus-proofs/, published under the Libertaria Unbound License (LUL-1.0).

Terminal window
# Build and verify all proofs
git clone https://git.sovereign-society.org/janus/janus-proofs
cd janus-proofs
lake build   # All theorems pass the Lean 4 kernel

No mathlib dependency. The proofs use only the Lean 4 standard library — keeping the dependency footprint minimal and the proof surface within reach of the future Janus Sovereign Prover (JSP) v2.0.

What This Doesn’t Prove (Yet)

Section titled “What This Doesn’t Prove (Yet)”

The proofs are about algorithmic models, not about the Zig implementation directly. They establish that:

  • ✅ The algorithms as designed are deterministic, confluent, and terminating
  • ✅ A refinement mapping documents how the models correspond to the Zig source
  • ❌ They do not prove the Zig code is bug-free
  • ❌ They do not catch memory-safety bugs in the compiler
  • ❌ They do not replace integration testing or fuzzing

The next step — a machine-checked refinement proof connecting the Lean models to the Zig implementation — is a longer-term goal that builds on this foundation.

Section titled “Related”