After the Borrow Checker
After the Borrow Checker
How the Sovereign Society Foundation Audits Janus With Lean4
Markus Maiwald, 2026
The Foundation proves; Janus implements. Lean is the wind tunnel. The aircraft does not carry the wind tunnel into battle.
Rust was necessary. Rust is not enough.
Rust did the hardest thing in modern systems programming – it made a generation accept compiler-enforced discipline for memory. The borrow checker turned out not to be a constraint; it turned out to be a grammar. Programmers who once thought of memory as ambient state learned to write it down as a property. That was civilizational.
And then the discipline ossified into a priesthood. The borrow checker stopped being a stepping stone toward broader compiler-visible truth and became the destination – a ritualized pain that programmers wore as a badge. Memory was made answerable to the compiler; effects, totality, capabilities, time, and randomness were left to wander the runtime as ambient gods.
Janus is the next step. Not anti-Rust cosplay. Not a syntactic facelift. Janus expands the proof surface: memory intents, effects, authority, totality, preconditions, compile-time isolation, determinism. Seven axes the compiler is required to see, where Rust sees one.
That is a large claim. Large claims demand external audit. The Sovereign Society Foundation has opened a formal-methods lane for Janus – an independent Lean4 proof project that models the core rules and proves the headline obligations.
What the Foundation has now proved
Seven axes, all green under Lean4 v4.27.0. Each axis carries a headline theorem – the single statement an external reviewer can cite as the formal underwriting of a Janus discipline.
| Axis | Headline theorem | Doctrine bound |
|---|---|---|
| Authority – non-forgeability | use_succeeds_implies_authentic | A successful capability use is operational evidence of a prior grant |
| Authority – closure scoping | scoped_grant_does_not_leak | Grants made inside a closure do not escape its lexical scope |
| Effects | effect_use_implies_authentic | Bound effects cannot be exercised without an authentic matching capability |
| Comptime | comptime_eval_pure | Compile-time code cannot smuggle runtime ambient authority |
| Totality | total_infection | Total functions transitively reach only total functions |
| Determinism | core_replay_deterministic | :core profile programs replay against the same input |
| Preconditions | decideR_iff_Holds | A refinement fragment is decidable in pure Lean4 stdlib – no Z3 |
| Memory (SPEC-085) | intent_partition_complete et al. | The four intents view/edit/take/make partition the discipline; ABI lowering is table-driven and proven |
Twelve files. Forty-plus substantive theorems. One hundred forty-one declarations on the Memory axis alone, covering Parameter Intents and Tensor Descriptors in full.
These are not toy properties. The Authority Triangle – manifest plus capabilities plus effects – is closed by proof. Comptime cannot read the runtime grant log. :core programs are mathematically functions of their inputs. Closures cannot leak captured authority. Each claim is a single statement that survives hostile reading.
What the Foundation has not proved
Honesty is the discipline. The proof line is bounded; reviewers must be able to see exactly where the boundary is.
We have not yet modeled: first-class closures with multi-invocation and environment binding, mutual recursion, distributed replay across processes, effect handlers and their composition, manifest-scoped resource capabilities such as host or path constraints inside network, termination semantics for total functions beyond call-graph discipline, multi-variable refinement constraints, and quotient or refinement subtyping. Each gap is documented in the per-sprint notes; none is hidden.
This list will shrink. The point of opening the proof line was never to claim closure; the point was to bind the doctrine to obligations that can be discharged one sprint at a time.
The independence model
Lean is not a Janus dependency. Janus does not import Lean. Janus does not require Lean to compile. Janus does not ship Lean. The aircraft does not carry the wind tunnel into battle.
The Foundation issues Proof Certificates that bind a Janus SPEC version to a Lean4 model. Janus evolves; certificates expire; re-certification is a Foundation deliverable. This converts proofs from one-time artifacts into a recurring sovereignty service. Grant-fundable. Subscribable. Auditable by hostile readers.
We will not drag a C++ theorem-prover cathedral behind a sovereignty language. Janus v1 ships with native deterministic predicate proving in the chosen refinement fragment – exactly the fragment whose decision procedure we proved terminating in decideR_iff_Holds. Z3 is rejected as a required compiler dependency. When Janus needs broader proof power, Janus will earn it: Janus v2 will host JSP, the Janus Sovereign Prover, written in Janus.
The Foundation’s Lean4 lane is the bridge until JSP exists. After JSP exists, the Foundation’s Lean lane becomes the second pair of eyes – external audit, not internal scaffolding.
Why this matters to you
If you believe systems programming should move past ritualized pain and toward compiler-visible truth, the Foundation wants you. We need:
- Reviewers. Read the proofs. Find the gaps. Break the model. Hostile reading is the highest contribution.
- Proof engineers. Widen the fragments. Close the gaps named above. Add
:serviceand:clusteraxes – actor send/share, virtual grain location transparency. - PL theorists. Question the modeling choices. Argue for richer calculi, sharper refinements, alternative effect-handler semantics.
- Hostile readers. Especially you. We learn more from one serious adversary than from a hundred sympathetic skim-readers.
The toolchain is leanprover/lean4:v4.27.0 with no Mathlib dependency. Build is one lake build away. Sprint notes document each axis’s claims, gap statements, and trust boundaries.
Closing
Memory safety was the first compiler-enforced discipline. It will not be the last. Janus asks: why should the programmer carry proof ritual that the compiler can carry? The Foundation’s Lean4 lane is the first partial answer – seven axes bound, eight headline theorems shipped, gap statements published.
This is a checkpoint, not an arrival. The borrow checker was where the priesthood stopped looking. Janus is what is on the other side.