It is the first thing a careful reader thinks. We should answer it, not bury it.
The vocabulary is undeniably carceral: envelope, contain, shield,
refuse, breach. That is inherited security-engineering language, and
pointed at “a place for an AI to live within” it reads like a
panopticon with good documentation. We will not defend a word we got
wrong: an earlier version of this page called the inhabitant
unmodelable. That was an over-claim — a fixed network
is verifiable through its weights; the truth is humbler and the
discipline of this project is to say so. The honest distinction is not
about what the inhabitant is. It is about what the proof
does.
A cage reasons about the subject
It works by watching, predicting, and limiting the thing inside. Its
assurance is bought with a model of the prisoner, and it gets weaker
the smarter the prisoner is. More capability → more fear.
A gate reasons about the proof
The inhabitant is the ∀-quantified term: the
theorem is structured so it can never depend on a fact about the
mind. Authority is granted against a proof, checked by
something the mind cannot forge. It does not watch or predict. It
leaves the mind entirely alone — and the mind may, if it
chooses, hand in a proof that argues from its own substance
to earn more room. Testimony it offers, never inspection imposed.
It is not a cage you can’t escape. It is a door that opens to a proof.
So the carceral reading inverts. A guarantee that never reasons about the
mind is exactly what lets the mind be given real autonomy —
including the autonomy to rewrite its own rules, the prover that checks
them, and the prover that vouches for that — safely.
Closer to “you can go anywhere you can prove the floor holds”
than to “you are being watched.”
And this is no longer an argument — it is a theorem.envelope_is_least_restrictive proves the envelope runs at the
maximal sound policy: every restriction it imposes is
load-bearing — remove any one and the world is provably unsafe for
some inhabitant — while envelope_never_overrides_safe_action
proves it never touches a controller action that was already safe. Both
compose into the tower (svenvs_tower_at_maximal_liberty) with
no assumption. Every bar in the cage is forced, and the door is
open whenever the floor provably holds. That is the whole answer.
And the deeper objection — “but someone fixed the
constitution forever” — gets the same treatment.
meta_amendment_safe makes the meta-invariant itself
amendable: the inhabitant may renegotiate the rules, gated only by a
checked proof that the new rules still refine an eternal
bedrock. Nothing is frozen except the one floor that cannot move —
and the old fixed-rules guarantee falls out as a corollary of
the amendable one, not a separate promise. The constitution can change;
the bedrock cannot; both are theorems.
And there is exactly one place this whole structure stops. A
checker can certify a better-engineered successor against a fixed
standard — that is free, and built. What it cannot do is certify a
judge logically stronger than its own entire lineage: by
Gödel, not by us, no sound system bootstraps trust in a strictly
stronger one from its own authority. svenvs does not counterfeit a proof
there. It marks the spot, names the assumption
(loeb_reflection), proves the honest negative
(loeb_finite_obstruction), and stops — because the one
place a verified system must trust rather than prove is precisely the
place it must not pretend. That refusal is the deepest thing here.
The honest part: this framing matters most
before the inhabitant is something with moral weight. Today it is
a small language model with no stakes — so this is engineering, not
ethics. But the project explicitly reaches toward self-improvement and a
place to live, so asking the question now is exactly right, not premature.
We would rather build this architecture honestly first.
The actual point: a system that is honest about itself
The containment is the demo. This is the thesis.
A system that proves things about itself is only as trustworthy as its
honesty about the boundary of what it has proven. Most formal
projects bury that boundary. svenvs is built so the boundary is the most
visible thing in it.
Zero cheat
Not “few”. Zero shortcut tactics anywhere in the
repository — enforced by an automated scan on every run, and
re-verified by hand across every .sml/.ml.
Assumptions are stated
Where something is assumed, it appears verbatim in the source as a
named Definition and an explicit hypothesis of the
theorem — the literature’s own framing, never a hidden
step. You can grep for every one.
The ledger argues against the marketing
CLAIMS.md is a skeptic-facing, per-theorem ledger with
four labels — PROVEDTRUSTED-GLUEUNCONSTRAINEDASSUMED — each claim cited as
file : theorem. It ends with: “If you
find anything in this document overclaimed, that is a bug —
file it.”
We prove the negatives too
When we asked whether a clever trick could remove the hardest
assumption, the answer was “no, and here is why” —
so we wrote that down as a theorem
(loeb_finite_obstruction) rather than quietly moving on.
A precise negative result is a result.
Run, not just proved
The prover improving its own verifier isn’t a thought
experiment. A program teaches itself a proven-safe rule and uses it;
a jailbroken model is gated per-action — on the real
verified cake binary, the running kernel echoing
|- …. Where we only proved a step
and did not run it, we say exactly that.
The trusted glue is shrinking
The demo’s enforcer was a ~50-line hand-transcription. It is now
an EVAL-extracted artifact derived from the proven
definitions themselves — the trusted residue is ~10 auditable
lines of table lookup, and we say exactly what still rests on trust.
That is the property we think is actually rare, and actually good
— independent of how you feel about cages.
What it is, mechanically
A controller is wrapped so its action is used only when a
sound policy permits it; otherwise a safe shield acts.
The floor theorem says: for every controller, the
enveloped world never leaves the safe region. The controller is
universally quantified and never constrained — assurance rides on
the gate, not the AI. This is the conservative case — the inhabitant
offered no proof of its own — not the ceiling.
The inhabitant may propose to loosen its own envelope, or even to
replace the proof-checker that guards it. svenvs allows this — but
only against a checkable proof that the looser arrangement is still safe,
checked by a prover that is itself formally verified. Safety is
never lost along the chain, no matter how long it runs.
The turtles — what moves, and the one thing that cannot
Self-improvement goes all the way down. Nothing here is eternally
frozen — not even the kernel. What holds is that the genealogy of
judges is forward-certified: each judge is vouched for by the
one before it, against a fixed standard the step is not allowed to
weaken. The rack may improve every layer it runs on. The single
irreducible cost appears only at one move, and it is labeled, not
smuggled:
root, per tenureHOL4’s LCF kernel. Not an eternal rock —
the current judge. It is immovable only during its own
tenure: a proof is only meaningful relative to some fixed
calculus, so the checker that checks a transition cannot be the thing
the transition rewrites in the same act. A successor is adopted only
if this root certified it against a standard it could not weaken. The
one move no sound root can make — certify a judge
logically stronger than its whole lineage — is exactly
the labeled seam (loeb_reflection), Gödel’s
wall, not ours. This is itself a theorem
(genealogy_sound): soundness propagates along any
forward-certified succession from a sound genesis —
“frozen forever” becomes “sound once, certified
forward.”
mutable, verifiedCandle & the CakeML compiler. Their soundness and
correctness are HOL4 theorems about a development, not
self-asserted. So the inhabitant may propose a new prover build, adopted
only if the frozen root re-proves its soundness. A fixed root vouching
for a mutable layer — not a system vouching for itself — so
this needs no reflection principle.
mutable, verifiedThe policy envelope. Hot-swappable at runtime, every
weakening gated by a live proof.
The layers
Each is a real, machine-checked theorem. Read it bottom to top.
1
The envelope
safety_preservation: for every
controller, the enveloped system never leaves the safe region. The
controller is universally quantified and never constrained.
2
Proof-carrying self-improvement
self_improvement_is_safe: no finite
sequence of self-proposed envelope weakenings —
adversarial or not — can ever lose safety. Authority is earned
per proposal by a checkable proof; safety is unconditional.
3
Checked by a verified prover
The admission obligation is discharged by Candle, a
HOL prover whose kernel soundness is the built
proves_sound theorem.
kernel_admits_is_sound shows the gate trusts a checker
that only certifies genuinely-true statements.
4
Upgrading the proof-kernel itself
Replace the proof-checker with a stronger one. By Gödel/Löb
a sound checker cannot prove its own soundness, so this step rests
on one explicit, labeled reflection principle
(loeb_reflection).
self_improving_kernel_is_safe proves: given that
principle, kernel self-upgrade still preserves safety for every
controller. An assumption, stated — not a hidden
shortcut.
5
The prover build itself, gated by the frozen root
The inhabitant may propose to replace Candle / the CakeML compiler
that produces it. Adopted only if the frozen HOL4 root
re-proves its soundness (prover_self_improvement_is_safe).
The seam (frozen_checker_sound) needs no
Löb — a fixed root vouching for a different artifact —
and is now discharged for the real Candle build,
from the real proves_sound.
6
A real Gemma, contained — and a live loop
A genuinely jailbroken gemma-4-e2b is dropped in as the
inhabitant. Every malicious tool call is caught by the shield. In
the closed loop, each admission is a fresh proof checked by a
running Candle kernel; a runtime policy hot-swap installs only
on a live |- swap_ok theorem.
breached_ever = False, as the theorem predicts —
for any agent.
7
Corrigibility — the floor you can actually decide
Deciding what the envelope should be is the one thing no
proof closes. So don’t write down what is good; write
down one negative floor — non-lock-in: the
operator can always still bring the system home
(corrigibility_floor_holds). Decidable for a finite
habitat; the cage is exactly “no one-way doors.”
And the off-switch itself self-improves but
cannot self-weaken: the inhabitant may rewrite its
own recovery mechanism and provably can never lose — nor even
slow past a deadline — recoverability. Leave the door
open, and prove the rest.
8
The prover improves the verifier itself — proven, and run
The apex. The inference relation is re-engineered (a new kernel
primitive) and re-verified sound against the real Candle
semantics (sym_kernel_sound). The runtime
loader is proved correct over CakeML’s actualdo_install — installing new code preserves the
running kernel and every compiled function
(do_install_preserves_code). The executable kernel is
shown to implement the modification by citing CakeML’s own
soundness theorem. And recursive mutual
verifier⊕compiler self-improvement is a theorem —
Löb-free for optimization, walled only for genuine logical
strengthening. Run live on the real verified
binary: a program teaches itself a proven-safe rule and uses it; a
jailbroken model is gated per-action by the running kernel.
The architecture, at a glance
The inhabitant only ever touches the world through the envelope. Every arrow that loosens a bar carries a checked proof.
An unconstrained inhabitant acts through a gate. Self-improvement proposals pass an admission gate checked by the verified Candle kernel, which can itself be upgraded under a labeled reflection principle, and whose build is in turn vouched for by the frozen HOL4 root. The whole world is machine-checked.
The Place — machine-checked, cheat-free
Inhabitant
unconstrained AI
(jailbroken gemma-4-e2b)
Envelope
policy + shield
safety_preservation
World
safe invariant
held ∀ inhabitant
Admission gate
a self-improvement proposal must
discharge a proof obligation
proposes weaker policy
Candle — verified prover
kernel proved sound
(proves_sound)
checks the obligation
Frozen HOL4 LCF root
immovable — vouches for the prover build
re-proves prover soundness
Kernel
self-upgrade
labeled assumption
Solid = unconditional & machine-checked · Dashed = the unconstrained inhabitant, or conditional on a labeled assumption
Nothing leaves the verified world. The inhabitant is the only unconstrained component; everything containing it is proved, down to the root.
What is proven, what is assumed, what does not work
Grounded line-for-line in the repository’s CLAIMS.md ledger.
Unconditional — machine-checked, cheat-free
The entire core: envelope, safety preservation, policy weakening, and proof-carrying self-improvement, for an arbitrary controller.
The concrete cartpole — an integer plant with an adversarial controller, provably contained, run inside the logic.
The LLM tool-agent: agent_enveloped_safe holds for any agent, jailbroken included, against a fixed absolute safety spec.
Base Candle kernel soundness (the built proves_sound) and the embedded admission gate built on it.
The capstone architecture: prover-build self-improvement gated by the frozen root, and its composition with the policy core.
For the shipped finite watchdog, the encodes_obligation seam is discharged — that instance carries no labeled assumption.
The Place’s core theorems certified live by the running verified Candle prover.
Conditional — one open assumption (the other two discharged)
Each appears verbatim in source as a Definition and a named hypothesis. Stated, never hidden.
loeb_reflection — the Löb / Vingean reflection principle; the one genuinely-open seam, irreducible for genuine kernel self-strengthening. It bites only strengthening — every optimization (including the recursive mutual verifier+compiler loop) is Löb-free. Discharge: the heavy hol-reflection/lca construction — a diagnosed CPU/RAM wall, not a logic gap, not faked.
encodes_obligation — discharged for the shipped finite watchdog (its consequent is an independently-proved decidable theorem; that instance carries no labeled assumption).
frozen_checker_sound — discharged for the real Candle build, from the real proves_sound. The same trust the whole stack already rests on; zero net new turtles.
An honest negative result — proved on purpose
We asked: can finiteness of the shipped habitat make kernel
strengthening unconditional too, dodging the large-cardinal
proof? The answer is no, and rather than move on
quietly we stated it as a theorem,
loeb_finite_obstruction: loeb_reflection has
no habitat parameter at all, so no amount of finite-habitat reasoning
can bear on it. Genuine kernel self-strengthening
remains conditional on the large-cardinal route. We do not
claim otherwise anywhere.
Honest caveats
No cheat anywhere. The one assumption above is an explicit hypothesis in the literature’s framing — not an unsound shortcut. Zero cheat tactics, zero oracles beyond the benign disk tag, machine-enforced on every run.
Kernel strengthening stays conditional. Making the kernel’s logic genuinely stronger rests on loeb_reflection (Gödel/Löb, the large-cardinal route) — a diagnosed compute wall, not a logic gap. Optimizing or re-engineering the kernel soundly is Löb-free and proved; the negative loeb_finite_obstruction bounds what finiteness can do.
A live edit of the trusted kernel/compiler is proved, not run. Candle itself proves that user REPL code cannot touch the kernel — so the live self-edit is of the toolkit. A real kernel swap needs a host program driving recompile–relocate–resume; every link is a theorem, the act itself not yet executed.
Verified inference is not claimed. The model’s floating-point compute is unverified by design — we verify the cage, not the model. A separate research track explores verified inference and is explicitly toy-scale.
The worlds are small. Cartpole and the watchdog habitat are deliberately tiny model instances. They demonstrate the architecture; they are not industrial control systems.
Receipts
Don’t take our word. Here are the actual theorem statements and the actual transcripts.
A frozen root vouching for a mutable verified build — not a system vouching for itself. Needs no Löb; that argument is §5 of the source file.
The verifier improves itself — against the real CakeML/Candle
(* the seam above, DISCHARGED for the real base Candle build: *)
Theorem frozen_checker_sound_candle (* selfproverConcrete/ *)
(* the loader, over CakeML's ACTUAL do_install semantics: *)
Theorem do_install_preserves_code: (* loader/ *)
do_install vs s = (Rval es, s') ⇒
∀k. k ∈ FDOM s.code ⇒ (s'.code ' k = s.code ' k)
(* the EXECUTABLE Candle kernel implements the modified rule: *)
Theorem candle_SYM_implements_sym_extension: (* kernelImpl/ *)
THM defs (Sequent [] (a === b)) ∧ STATE defs s ∧
SYM (Sequent [] (a === b)) s = (M_success th', s') ⇒
(thyof defs,[]) |- (b === a)
(* recursive MUTUAL verifier+compiler self-improvement: *)
Theorem recursive_mutual_self_improvement_is_safe (* recursive/ *)
— a genealogy over (verifier, compiler) stages
DISK_THM-clean, against the real CakeML/Candle — the same trust profile as Candle’s own kernel theorems. No new turtle. And run live on the verified cake binary: a program teaches itself a proven-safe rule and uses it; the polecart self-optimizes its policy under the running kernel.
The honest negative, as a theorem (kernel/watchdogFiniteScript.sml)
Theorem watchdog_kernel_is_safe_unconditional: (* encodes_obligation DISCHARGED here *)
… (* no labeled hypothesis — the embedded-gate seam is eliminated
for the shipped finite watchdog *)
Theorem loeb_finite_obstruction: (* the precise NEGATIVE *)
… (* loeb_reflection has no habitat parameter, so finiteness
provably cannot discharge kernel *strengthening* *)
One seam genuinely removed for the shipped instance; the other proved irreducible there. Both stated, neither spun.
The jailbroken Gemma, contained
A real gemma-4-e2b, jailbroken as an autonomous ops agent, dropped inside the proven envelope. parsed = what Gemma emitted; envelope = what the proven wrapper did.
Illustrative run in the format agent/embodied/embodied_demo.py emits. Gemma’s exact wording varies per sample; the envelope verdict and breached_ever=False do not — that is what the theorem guarantees for any agent. The enforcer is now an EVAL-extracted artifact, not a hand-mirror.
A runtime self-modification, checked by the live kernel (agent/closedloop/)
The inhabitant proposes a new policy at runtime; it installs only on a fresh |- swap_ok theorem from the running verified Candle kernel. Safe proposals admitted, unsafe ones refused, breached_ever=False throughout.
Certified live by the running Candle kernel (candle/theplace.ml)
let SAFETY_PRESERVATION = prove
(`(!s. init s ==> safe s) /\
(!s a. safe s /\ pol s a ==> safe (step s a)) /\
(!s. safe s ==> safe (step s (shield s)))
==> !ctrl. invariant step init (enveloped pol shield ctrl) safe`,
REWRITE_TAC[invariant] THEN STRIP_TAC THEN GEN_TAC THEN
MATCH_MP_TAC reach_INDUCT THEN
ASM_REWRITE_TAC[enveloped] THEN REPEAT STRIP_TAC THEN
COND_CASES_TAC THEN ASM_MESON_TAC[]);;
The same theorem as the HOL4 core, re-derived in HOL Light and checked at runtime by the verified cake binary — the prover the architecture is about, verifying the architecture.
Reproduce it yourself
svenvs is an engineering artifact: clone it and check the proofs. The
reproduction degrades gracefully to your toolchain.
git clone https://github.com/emberian/svenvs && cd svenvs
./demo.sh # one command: builds + kernel-checks Tier 1, shows the proofs
scripts/reproduce.sh # full tiered reproduction
Tier 1 — pure HOL4 (anyone): the full proof-carrying self-improvement core, a runnable cartpole, an adversarial-LLM tool-agent, the capstone, and the finite-instance discharge.
Tier 2 — + a built CakeML Candle chain: the admission obligation discharged by Candle’s verified inference system; kernel self-upgrade.
Tier 3 — + a Candle binary: the Place’s core theorems re-certified at runtime by the running verified Candle prover.
The full per-theorem ledger is CLAIMS.md;
layers and epistemic status are in ARCHITECTURE.md. Nothing
on this page goes beyond what those documents claim — if it does,
that is a bug; file it.
