diff --git a/docs/build-content.py b/docs/build-content.py
index c106a6cc9..4f7a252a6 100644
--- a/docs/build-content.py
+++ b/docs/build-content.py
@@ -43,7 +43,7 @@
"features/": ("2026-10-21", "21f5c8dddb47df96"),
"manual/": ("2026-10-21", "0f7e605dc087544d"),
"pitch/": ("2026-10-21", "7cfe9803d7d11df5"),
- "demo/": ("2026-10-21", "317b8850ecc3c5de"),
+ "demo/": ("2026-10-22", "9dae5fe7a3dbf01b"),
"guides/": ("2026-10-21", "888b965163695896"),
"guides/build-and-verify-a-web-app/": ("2026-10-21", "0b0d7ae775899b60"),
"guides/red-team-a-web-app/": ("2026-10-21", "3af532e9ff5592f3"),
diff --git a/docs/demo/README.md b/docs/demo/README.md
index b8378fe9a..fc36c793e 100644
--- a/docs/demo/README.md
+++ b/docs/demo/README.md
@@ -1,22 +1,28 @@
-# h5i demo: Build → Verify → Red-team → Regression
+# h5i demo: Build → Verify → Test the running app → Regression
-The 60-second film is a deterministic HTML timeline, rendered to MP4. It keeps
+The 80-second film is a deterministic HTML timeline, rendered to MP4. It keeps
the opening question and the shell, console, editor, and browser windows. The
agent follows one board application through four stages.
| Time | Beat |
| --- | --- |
| 0:00–0:07 | Opening question and the Build and Verify Your Web Apps title card. |
-| 0:07–0:13 | Build: the agent writes the board's Rust kernel. |
-| 0:13–0:29 | Verify: extract to Lean 4, show `authorized`, run proof and the configured mutation, then reveal the kernel proof boundary. |
-| 0:29–0:49 | Red-team: open the same board in a browser, replay Alice's request with Bob's post ID, and record the adapter finding. |
-| 0:49–0:56 | Regression: fix the adapter's visibility check and replay a YAML test; Alice gets 200 and Bob's private post returns 403. |
-| 0:56–1:00 | Close: Build and Verify Your Web Apps. with h5i. The Verifiable Web Framework for Rust. |
+| 0:07–0:19 | Build: a large editor shows the board's Rust delete permission check. |
+| 0:19–0:28 | Extract: Charon and Aeneas visibly generate the Lean 4 author and moderator branches from Rust, then the full generated definition appears. |
+| 0:28–0:42 | Verify: read the `authorized` theorem, its `writes_of` case split, and the scripted Lean check result. |
+| 0:42–0:52 | Explore: the theorem dependency graph follows the real Lean lemmas, then states the kernel write proof boundary. |
+| 0:52–1:09 | Test the running board end to end with Development Infrastructure. Its red-teaming tool reveals the HTTP read flaw. |
+| 1:09–1:16 | Regression: fix the adapter's visibility check and replay a YAML test; Alice gets 200 and Bob's private post returns 403. |
+| 1:16–1:20 | Close: Build and Verify Your Web Apps. with h5i. The Verifiable Web Framework for Rust. |
The Rust kernel and Lean theorem names shown are drawn from
`examples/app/board`. Its `authorized` theorem concerns successful **kernel
-writes**. The private-post `GET /api/posts/{id}` route, its IDOR, and the
-adapter fix are an **illustrative scenario** for this film; that route is not
+writes**. The dependency graph shows only dependencies present in the board's
+Lean proof. `h5i app check examples/app/board` records `delete_spec → writes_of`,
+`writes_of → authorized`, and `other_mod → authorized` in its declaration
+catalog; the film renders that small, fixed subset. The private-post
+`GET /api/posts/{id}` route, its IDOR, and the adapter fix are an
+**illustrative scenario** for this film; that route is not
present in the checked-in board server, and no live finding or regression run
is claimed. The UI labels the scenario. This distinction matters: a proof of
kernel writes cannot establish the behavior of a separate HTTP read route.
@@ -39,7 +45,7 @@ Rendering needs ffmpeg, Playwright, and Chromium:
```bash
node render.mjs --scale 1 --out-height 1080 --fps 24 --crf 20 --preset veryfast
-node render.mjs --stills 10,26,37,43,52 --scale 1
+node render.mjs --stills 14,20,22,25,34,45,50,64,73 --scale 1
```
The page is fingerprinted by `docs/build-content.py`; changes require an
diff --git a/docs/demo/index.html b/docs/demo/index.html
index 40f6ae940..ab4054dab 100644
--- a/docs/demo/index.html
+++ b/docs/demo/index.html
@@ -3,32 +3,32 @@
-Build and Verify Your Web Apps | h5i 60-second demo
-
+Build and Verify Your Web Apps | h5i demo
+
-
+
-
+
@@ -108,17 +108,56 @@
#win-shell{left:40px;top:160px;width:600px;height:760px}
#win-con{left:670px;top:160px;width:1210px;height:760px}
#win-app{left:1130px;top:528px;width:730px;height:376px;z-index:3}
- #win-ed{left:1130px;top:528px;width:730px;height:376px;z-index:3}
+ #win-ed{left:150px;top:170px;width:1620px;height:704px;z-index:5}
+ #desk.code-focus #win-shell,#desk.code-focus #win-con{opacity:.12!important}
+ #desk.code-focus #win-ed{box-shadow:0 36px 110px rgba(0,0,0,.88)}
.etabs{flex:none;display:flex;gap:2px;padding:8px 10px 0;background:var(--w-surface);border-bottom:1px solid var(--w-line)}
.etab{padding:6px 12px 8px;font-family:var(--w-mono);font-size:13px;color:var(--w-ink3);border-bottom:2px solid transparent;margin-bottom:-1px;white-space:nowrap}
.etab.cur{color:var(--w-ink);border-bottom-color:var(--w-accent)}
.etab i{font-style:normal;margin-left:8px;font-size:11px;letter-spacing:.1em;text-transform:uppercase;color:var(--w-accent)}
- .code{display:none;flex:1;padding:12px 16px;font-family:var(--w-mono);font-size:13.5px;line-height:1.5;overflow:hidden}
+ .code{display:none;flex:1;padding:28px 38px;font-family:var(--w-mono);font-size:20px;line-height:1.55;overflow:hidden}
+ #ed-thm{font-size:18.5px;line-height:1.65}
.code.on{display:block}
.cl{display:flex;gap:14px;white-space:pre;opacity:0}
.cl.on{opacity:1}
- .cl .n{width:22px;text-align:right;color:var(--w-ink4);flex:none;font-size:12px;padding-top:2px}
+ .cl .n{width:32px;text-align:right;color:var(--w-ink4);flex:none;font-size:15px;padding-top:3px}
.cl .c{color:var(--w-ink)} .kw{color:var(--w-violet)}
+ .cl.focus .c{color:#fff;background:rgba(52,211,153,.12);box-shadow:0 0 0 5px rgba(52,211,153,.12);border-radius:2px}
+ .cl.focus .c .kw{color:var(--w-green)}
+ #extract-view{position:absolute;inset:81px 0 0;z-index:2;padding:42px 48px;background:#0b0e12;opacity:0;pointer-events:none}
+ .extract-heading{display:flex;align-items:center;justify-content:space-between;font-family:var(--w-mono);font-size:17px;color:var(--w-ink2)}
+ .extract-heading b{color:var(--w-accent);font-weight:700}
+ .extract-columns{display:grid;grid-template-columns:1fr 132px 1fr;gap:26px;align-items:stretch;margin-top:28px;height:385px}
+ .extract-pane{padding:26px 25px;border:1px solid var(--w-line2);border-radius:11px;background:#12161b;overflow:hidden}
+ .extract-pane.generated{border-color:rgba(81,208,210,.5)}
+ .extract-label{font-family:var(--w-mono);font-size:14px;letter-spacing:.08em;color:var(--w-ink3);text-transform:uppercase;margin-bottom:22px}
+ .extract-label strong{color:var(--w-ink);font-weight:400;letter-spacing:0;text-transform:none}
+ .extract-pane pre{font-family:var(--w-mono);font-size:17px;line-height:1.8;white-space:pre;color:var(--w-ink)}
+ .extract-pane .mark{color:var(--w-green)}
+ .extract-flow{display:flex;flex-direction:column;align-items:center;justify-content:center;gap:18px;font-family:var(--w-mono);font-size:13px;color:var(--w-ink3);text-align:center}
+ .extract-flow .arrow{font-size:48px;color:var(--w-accent);text-shadow:0 0 22px var(--w-accent)}
+ .extract-line{display:block;opacity:0;transform:translateX(-12px)}
+ .extract-progress{display:flex;align-items:center;gap:22px;margin-top:26px;font-family:var(--w-mono);font-size:16px;color:var(--w-ink2)}
+ .extract-progress span{width:245px;color:var(--w-accent)}
+ .extract-track{flex:1;height:7px;border-radius:7px;background:#252a30;overflow:hidden}
+ #extract-fill{height:100%;width:0;background:linear-gradient(90deg,var(--w-accent),#51d0d2);box-shadow:0 0 20px #51d0d2}
+ #extract-done{width:230px;text-align:right;color:#51d0d2}
+ #proof-status{position:absolute;right:42px;bottom:34px;padding:17px 24px;border:1px solid rgba(52,211,153,.55);border-radius:10px;background:#10241e;color:var(--w-green);font-family:var(--w-mono);font-size:19px;opacity:0}
+ #proof-status small{display:block;color:var(--w-ink2);font-size:14px;margin-top:5px}
+ #win-graph{left:250px;top:195px;width:1420px;height:640px;z-index:6}
+ .graph-head{padding:25px 34px 16px;border-bottom:1px solid var(--w-line)}
+ .graph-head h3{font-size:29px;letter-spacing:-.02em}
+ .graph-head p{font-size:16px;color:var(--w-ink2);margin-top:5px}
+ .graph-body{position:relative;flex:1;background-image:radial-gradient(#292d34 1px,transparent 1px);background-size:21px 21px}
+ .graph-body svg{position:absolute;inset:0;width:100%;height:100%;overflow:visible}
+ .graph-edge{fill:none;stroke:#51d0d2;stroke-width:3;opacity:.9}
+ .graph-node{position:absolute;width:255px;min-height:92px;padding:15px 18px;border:1px solid #4d5668;border-radius:10px;background:#171a20;box-shadow:0 15px 35px rgba(0,0,0,.45)}
+ .graph-node b{display:block;font-family:var(--w-mono);font-size:20px;color:#f0eef8}
+ .graph-node small{display:block;margin-top:7px;font-size:14px;color:var(--w-ink2)}
+ .graph-node.selected{border:2px solid var(--w-accent);background:#252025}
+ .graph-node.source{border-color:#51d0d2}
+ .graph-foot{padding:13px 34px;color:var(--w-ink2);font-size:15px;border-top:1px solid var(--w-line)}
+ .graph-foot b{color:var(--w-green)}
.agent{flex:none;display:flex;align-items:center;gap:16px;padding:14px 20px 10px;border-bottom:1px solid var(--w-line)}
.mascot{margin:0;font-family:var(--w-mono);font-size:13px;line-height:1.05;color:#e0241b;text-shadow:0 0 14px rgba(224,36,27,.5)}
.who{font-size:15px;color:var(--w-ink2)} .who b{color:var(--w-ink);font-weight:600}
@@ -394,9 +433,9 @@
Each row is a statement about the extracted kernel. It holds for the running app only within the trust boundary.
-
theorem
statement
status
mutants
+
theorem
statement
status
scope
-
authorizedTheorems.lean:79
Every write a successful command makes is allowed by the policy.
unconfirmedproven
kernel
+
authorizedTheorems.lean:79
Every write a successful command makes is allowed by the policy.
unconfirmedproven
kernel writes
inv_preservedTheorems.lean:160
Invariants hold in every state the board can reach.
unconfirmedproven
kernel
transition_totalTheorems.lean:55
The kernel transition returns a result for every command.
unconfirmedproven
kernel
@@ -408,8 +447,7 @@
extractionokBoardKernel.lean matches kernel/src/lib.rs · no drift
Lean 4ok3 shown theorems · 0 sorry
axiom gateokpropext, Quot.sound, Classical.choice only
-
mutant1 of 1 caughtconfigured kernel mutation broke a proof
if p.author == user ||
+ is_moderator(&s.moderators, user) {
+ Ok((one(Write::DelPost(id)),
+ Reply::Done))
+} else {
+ Err(Error::Forbidden)
+}
+
Charon→Aeneas
+
Generated · BoardKernel.lean
if p.author = userthen let v ← one (Write.DelPost id) …else let b ← is_moderator s.moderators user if b … else ok (core.result.Result.Err Error.Forbidden)
/* the camera: a framing per beat, hard cuts between. The desk is drawn at stage size, so 1 is "see everything";
a zoom pushes toward the console and leaves most of the shell in frame. */
const shots = [
- {a:T.ws, b:T.tEvidence, from:{x:0,y:0,s:1}, to:{x:0,y:0,s:1}},
+ {a:T.ws, b:T.graph, from:{x:0,y:0,s:1}, to:{x:0,y:0,s:1}},
+ {a:T.graph, b:T.tEvidence, from:{x:0,y:0,s:1}, to:{x:0,y:0,s:1}},
{a:T.tEvidence, b:T.hack, from:{x:-70,y:40,s:1.1}, to:{x:-70,y:40,s:1.1}},
{a:T.hack, b:T.tFindings, from:{x:0,y:0,s:1}, to:{x:0,y:0,s:1}},
{a:T.tFindings, b:T.tBoxes, from:{x:-70,y:40,s:1.1}, to:{x:-70,y:40,s:1.1}},
@@ -545,15 +613,14 @@
Private postssigned in as Alice
/* the agent's shell. Outputs are scripted, not a live scan or build. */
const term = [
{at:T.write+.2, out:[`✎ writing examples/app/board/kernel/src/lib.rs`]},
- {at:T.write+2.6, out:[`✎ delete: only author or moderator may remove a post`]},
+ {at:T.write+4.0, out:[`✎ delete: only author or moderator may remove a post`]},
{at:T.extract+.2, cmd:'h5i app extract examples/app/board', cps:70},
{at:T.extract+1.3, out:[`Charon + Aeneas · Rust kernel → generated Lean 4`]},
{at:T.prove+.2, out:[`✎ theorem authorized: successful writes follow the policy`]},
- {at:T.prove+2.0, out:[`✎ proofs/Theorems.lean checks the extracted kernel`]},
+ {at:T.prove+2.0, out:[`✎ writes_of splits six command cases; authorized checks each write`]},
{at:T.verify+.2, cmd:'h5i app prove examples/app/board', cps:70},
{at:T.verify+1.4, out:[`Lean 4 passed · authorized · inv_preserved · transition_total`]},
- {at:T.verify+2.1, cmd:'h5i app mutate examples/app/board', cps:70},
- {at:T.verify+3.5, out:[`1/1 configured kernel mutation caught by proofs`]},
+ {at:T.graph+.4, out:[`authorized uses writes_of and other_mod`]},
{at:T.hack+.3, clear:true},
{at:F+.5, cmd:'h5i browser open http://board.local/posts', cps:74},
{at:F+1.7, out:[`✔ session audit-42 · signed in as Alice`]},
@@ -589,6 +656,7 @@
Private postssigned in as Alice
/* the pointer: moves to a tab, clicks it */
const clicks = [
{at:T.tApps, target:'ri-apps'},
+ {at:T.graph, target:'g-authorized'},
{at:T.tEvidence, target:'tab-evidence'},
{at:T.hack, target:'ri-sessions'},
{at:T.tFindings, target:'tab-findings'},
@@ -601,8 +669,8 @@
Private postssigned in as Alice
}
function drawPointer(t) {
const p = $('ptr');
- if (t < T.tEvidence - 1.2 || t >= T.close) { p.style.opacity = 0; return; }
- let from = {x: 1500, y: 470}, to = from, moveAt = T.tEvidence - 1.2, clickAt = Infinity;
+ if (t < T.graph - 1.2 || t >= T.close) { p.style.opacity = 0; return; }
+ let from = {x: 1500, y: 470}, to = from, moveAt = T.graph - 1.2, clickAt = Infinity;
for (let i = 0; i < clicks.length; i++) {
const c = clicks[i]; const start = c.at - .9;
if (t >= start) { from = i ? centerOf(clicks[i-1].target) : from; to = centerOf(c.target); moveAt = start; clickAt = c.at; }
@@ -653,16 +721,32 @@
Private postssigned in as Alice
$('tab-theorems').classList.toggle('cur', atab === 'theorems'); $('tab-evidence').classList.toggle('cur', atab === 'evidence');
on('p-theorems', atab === 'theorems'); on('p-evidence', atab === 'evidence');
[T.verify+1.4, T.verify+1.8, T.verify+2.2].forEach((at, i) => { const r = $('th'+(i+1)); r.classList.toggle('proven', t >= at); });
- const rcpt = t >= T.verify + 3.5;
+ const rcpt = t >= T.verify + 1.4;
vis('pl-norcpt', !rcpt); vis('pl-rcpt', rcpt); $('n-rcpt').textContent = rcpt ? 1 : 0;
- [1,2,3,4,5].forEach(i => on('ev'+i, t >= T.tEvidence + .3 + i*.22));
+ [1,2,3,4].forEach(i => on('ev'+i, t >= T.tEvidence + .3 + i*.22));
// the editor: the agent writes Rust, Aeneas writes Lean, the agent writes the proof
- const etab = t >= T.prove ? 'thm' : t >= T.extract + 1.2 ? 'lean' : 'rs';
+ const etab = t >= T.prove ? 'thm' : t >= T.extract + 4.2 ? 'lean' : 'rs';
$('et-rs').classList.toggle('cur', etab === 'rs'); $('et-lean').classList.toggle('cur', etab === 'lean'); $('et-thm').classList.toggle('cur', etab === 'thm');
on('ed-rs', etab === 'rs'); on('ed-lean', etab === 'lean'); on('ed-thm', etab === 'thm');
- for (let i = 0; i < 14; i++) on('rs'+i, t >= T.write + .4 + i*.22);
- for (let i = 0; i < 5; i++) on('le'+i, t >= T.extract + 1.5 + i*.25);
- for (let i = 0; i < 8; i++) on('tl'+i, t >= T.prove + .4 + i*.6);
+ for (let i = 0; i < 14; i++) on('rs'+i, t >= T.write + .4 + i*.35);
+ for (let i = 0; i < 17; i++) on('le'+i, t >= T.extract + 1.5 + i*.26);
+ for (let i = 0; i < 8; i++) on('tl'+i, t >= T.prove + .4 + i*.7);
+ // Charon and Aeneas turn the visible Rust branch into Lean, frame by frame.
+ const ex = $('extract-view'), progress = ramp(t, T.extract+.3, 3.3);
+ ex.style.opacity = t < T.extract || t >= T.extract+4.7 ? 0 :
+ eo(ramp(t,T.extract,.4)) * (1-ramp(t,T.extract+4.1,.6));
+ $('extract-fill').style.width = `${progress*100}%`;
+ $('extract-done').textContent = progress >= 1 ? 'BoardKernel.lean generated' : 'generating…';
+ $('extract-arrow').style.transform = `translateX(${Math.sin(t*9)*5}px)`;
+ ex.querySelectorAll('.extract-line').forEach((line,i) => {
+ const q = eo(ramp(t,T.extract+.75+i*.27,.45));
+ line.style.opacity = q;
+ line.style.transform = `translateX(${(1-q)*-12}px)`;
+ });
+ $('proof-status').style.opacity = t >= T.verify+1.4 && t < T.graph ? eo(ramp(t,T.verify+1.4,.5)) : 0;
+ for (const id of ['rs5','rs6']) $(id).classList.toggle('focus', t >= T.write+5 && t < T.extract);
+ for (const id of ['le8','le13','le14']) $(id).classList.toggle('focus', t >= T.extract+5 && t < T.prove);
+ $('tl2').classList.toggle('focus', t >= T.prove+5 && t < T.graph);
}
/* dust: a seeded field of motes drifting upward, parallaxed against the camera */
@@ -698,16 +782,17 @@
Private postssigned in as Alice
/* the one line of narration, as a lower third */
const caps = [
- {at:T.write+.6, html:`Build the board's Rust kernel and HTTP app.`},
- {at:T.extract+.6, html:`Verify the extracted kernel with Lean 4.`},
- {at:T.prove+.6, html:`Theorem authorized covers successful kernel writes.`},
- {at:T.verify+.6, html:`Lean checks the proof; mutations test whether it detects changed logic.`},
- {at:T.tEvidence+.6, html:`Verified kernel: Lean 4 proves authorization of kernel writes.`},
- {at:T.hack+.6, html:`Unverified HTTP adapter: red-team the same app's read route.`},
- {at:F+5.8, html:`Replay Alice's request with Bob's post ID.`},
- {at:T.tFindings+.6, html:`Finding: red-teaming exposes a read route that bypasses kernel policy.`},
- {at:T.deny+.3, html:`Fix the adapter's visibility check, then replay the request.`},
- {at:T.tBoxes+.6, html:`Regression: Alice gets 200; Bob's private post returns 403.`},
+ {at:T.write+.6, html:`Only authors or moderators can delete posts.`},
+ {at:T.extract+.6, html:`Rust is extracted into Lean 4.`},
+ {at:T.prove+.6, html:`authorized covers successful kernel writes.`},
+ {at:T.verify+.6, html:`Lean checks the proof.`},
+ {at:T.graph+.6, html:`Follow the lemmas behind authorized.`},
+ {at:T.tEvidence+.6, html:`The proof covers kernel writes.`},
+ {at:T.hack+.6, html:`Development Infrastructure tests the app end to end.`},
+ {at:F+5.8, html:`Its red-teaming tool replays Alice's read for Bob's post.`},
+ {at:T.tFindings+.6, html:`The HTTP read route exposes Bob's private post.`},
+ {at:T.deny+.3, html:`Fix the route and save the replay as a test.`},
+ {at:T.tBoxes+.6, html:`The regression passes. Alice gets 200; Bob gets 403.`},
];
function renderCap(t) {
let i = -1; for (let k = 0; k < caps.length; k++) if (t >= caps[k].at) i = k;
@@ -756,12 +841,15 @@