Proof scope, baselines, coverage, prior art and qualification path

scripts/seo/config.mjs

@@ -6,7 +6,7 @@ export default {
   drop: ['script', 'style', 'button', 'form', '.prevnext'],
   title: 'Mru docs',
   summary:
-    "Reference for Mru's open core: the shrinking-quorum decision crate and its fault-injection demo (Rust, no_std, four Kani proofs), the Dusk simulator and the Mru 2049 browser flight simulator. Prototype at TRL 3; code under Apache 2.0.",
+    "Reference for Mru's open core, for unattended missions with no repair path: the shrinking-quorum decision crate and its fault-injection demo (Rust, no_std, nine Kani proofs: four on the core, five on the C interface), the Dusk simulator and the Mru 2049 browser flight simulator. Prototype on general-purpose processors, not flight hardware; code under Apache 2.0.",
   intro:
     'Product pages, use cases and research results are at https://mru.space/llms.txt. Questions: contact@mru.space.',
   sections: [

scripts/sync-tokens.mjs

@@ -21,6 +21,11 @@ const FILES = [
   ]),
   ['src/scripts/theme.ts', 'src/scripts/theme.ts'],
   ['src/components/Breadcrumbs.astro', 'src/components/Breadcrumbs.astro'],
+  // Headline numbers: claims.json is generated in the website from the flight
+  // and dusk results files. Docs pages read them with claim() or <Claim />.
+  ['src/data/claims.json', 'src/data/claims.json'],
+  ['src/data/claims.ts', 'src/data/claims.ts'],
+  ['src/components/Claim.astro', 'src/components/Claim.astro'],
   // Shared build scripts: share cards, Markdown twins and llms files, checks.
   // Each repo keeps its own scripts/seo/config.mjs.
   ...[

src/components/Claim.astro

@@ -0,0 +1,15 @@
+---
+// A number from claims.json, for MDX and templates: <Claim id="dusk.work_vs_tmr" />.
+// part="ci" gives the interval, part="min" the lowest seed.
+import { claim } from '../data/claims';
+interface Props {
+  id: string;
+  part?: 'text' | 'ci' | 'min';
+}
+const { id, part = 'text' } = Astro.props;
+const c = claim(id);
+const out = part === 'ci' ? c.ci : part === 'min' ? c.min_text : c.text;
+if (out === undefined) throw new Error(`claims.json: claim "${id}" has no ${part}`);
+---
+
+<Fragment set:text={out} />

src/data/claims.ts

@@ -0,0 +1,57 @@
+// Headline numbers, read from claims.json, which scripts/claims/pull.mjs
+// writes from the results files in mruspace/flight and mruspace/dusk.
+// A page asks for a claim by id; an unknown id fails the build.
+import data from './claims.json';
+
+export interface Claim {
+  value: unknown;
+  format: string;
+  text: string;
+  ci?: string;
+  min_text?: string;
+  unit: string;
+  scope: string;
+  conditions: string;
+  source: { repo: string; path?: string; kind?: string; ref?: string; command?: string };
+  /** The results-file row a claim came from, when a page shows more than one number from it. */
+  detail?: Record<string, unknown>;
+}
+
+export const CLAIMS = data.claims as unknown as Record<string, Claim>;
+export const CLAIM_SOURCES = data.sources;
+
+export function claim(id: string): Claim {
+  const c = CLAIMS[id];
+  if (!c) throw new Error(`claims.json: no claim "${id}". Run npm run claims, or fix the id.`);
+  return c;
+}
+
+/** The claim's text, for templates: {t('dusk.work_vs_tmr')} gives "1.34×". */
+export const t = (id: string): string => claim(id).text;
+
+/** "1.33× to 1.35×" for a claim with an interval. */
+export function ci(id: string): string {
+  const c = claim(id);
+  if (!c.ci) throw new Error(`claims.json: claim "${id}" has no interval`);
+  return c.ci;
+}
+
+// Static copy (metadata descriptions, research frontmatter) cannot call t().
+// assertClaims checks it instead: every listed claim's text must appear, and
+// every decimal or grouped number in the copy must belong to a listed claim.
+// Decimals and grouped integers; version strings such as 0.2.0 are not claims.
+const NUM = /(?<![\d.])\d+\.\d+(?![.\d])|\d{1,3}(?:,\d{3})+/g;
+const norm = (s: string) => s.replace(/(\d)x\b/g, '$1×');
+export function assertClaims(where: string, strings: (string | undefined)[], ids: string[] = []): void {
+  if (ids.length === 0) return;
+  const copy = norm(strings.filter(Boolean).join('\n'));
+  const allowed = new Set<string>();
+  for (const id of ids) {
+    const c = claim(id);
+    if (!copy.includes(c.text) && !copy.includes(c.text.replace('×', '')))
+      throw new Error(`claims: ${where} lists ${id} ("${c.text}") but its copy does not contain it`);
+    for (const s of [c.text, c.ci, c.min_text]) for (const n of (s ?? '').match(NUM) ?? []) allowed.add(n);
+  }
+  for (const n of copy.match(NUM) ?? [])
+    if (!allowed.has(n)) throw new Error(`claims: ${where} has the number "${n}", which no listed claim gives`);
+}

src/data/metadata.json

@@ -10,7 +10,7 @@
   {
     "url": "https://docs.mru.space/concepts/shrinking-quorum/",
     "title": "Shrinking quorum · Mru Docs",
-    "description": "Vote on three replicas, compare on two, self-check on one. The rule, its Kani-proved guarantees, its cost, and how replicas are diagnosed.",
+    "description": "Vote on three replicas, compare on two, self-check on one. What Kani proves per tick, what is tested per run, the cost and the command path.",
     "ogTitle": "Shrinking quorum",
     "cardLabel": "Docs · Concepts",
     "schema": ["TechArticle", "BreadcrumbList"]
@@ -23,10 +23,26 @@
     "cardLabel": "Docs · Concepts",
     "schema": ["TechArticle", "BreadcrumbList"]
   },
+  {
+    "url": "https://docs.mru.space/concepts/prior-art/",
+    "title": "Prior art and related work · Mru Docs",
+    "description": "TMR, degradable systems, Byzantine agreement, Space Shuttle redundancy management and deep-space fault protection, and how Mru relates.",
+    "ogTitle": "Prior art and related work",
+    "cardLabel": "Docs · Concepts",
+    "schema": ["TechArticle", "BreadcrumbList"]
+  },
+  {
+    "url": "https://docs.mru.space/concepts/qualification/",
+    "title": "Qualification path · Mru Docs",
+    "description": "What exists for Mru against NPR 7150.2, NASA-STD-8739.8, ECSS-E-ST-40C and ECSS-Q-ST-80C, and what has not started. No compliance claim.",
+    "ogTitle": "Qualification path",
+    "cardLabel": "Docs · Concepts",
+    "schema": ["TechArticle", "BreadcrumbList"]
+  },
   {
     "url": "https://docs.mru.space/core/quorum-crate/",
     "title": "quorum crate API reference · Mru Docs",
-    "description": "API reference for the quorum crate: Policy, Mode, Reply, Outcome, Verdict, decide(), Health. no_std, no allocation, four Kani proofs.",
+    "description": "API reference for the quorum crate: Policy, Mode, Reply, Outcome, Verdict, decide(), Health. no_std, no allocation, nine Kani proofs.",
     "ogTitle": "The quorum crate",
     "cardLabel": "Docs · Core runtime",
     "schema": ["TechArticle", "SoftwareSourceCode", "BreadcrumbList"]
@@ -58,7 +74,7 @@
   {
     "url": "https://docs.mru.space/simulation/dusk/",
     "title": "Dusk simulator reference · Mru Docs",
-    "description": "Run Dusk, the Monte Carlo of redundancy policies: options and defaults, the fault model, default results, sweeps and what it does not claim.",
+    "description": "Run Dusk, the Monte Carlo of redundancy policies: options, the fault model, results and their definitions, sweeps, ground support and limits.",
     "ogTitle": "Dusk",
     "cardLabel": "Docs · Simulation",
     "schema": ["TechArticle", "SoftwareSourceCode", "BreadcrumbList"]

src/data/nav.ts

@@ -1,5 +1,10 @@
 // Docs navigation, from the DocsNav artboard. The nav follows concepts and
 // layers, not repository names. Prev/next follow PAGES.
+//
+// A page marks one item active: the item for the page itself. Items that link
+// to a section of a page (an href with #) are never active; the page item is.
+// So on /concepts/shrinking-quorum/ "Shrinking quorum" is active, not
+// "Degradation-first" or "Graceful Degradation Index".
 
 export type NavId =
   | 'home'
@@ -8,6 +13,8 @@ export type NavId =
   | 'quorum'
   | 'gdi'
   | 'layers'
+  | 'prior'
+  | 'qual'
   | 'crate'
   | 'cli'
   | 'proofs'
@@ -36,10 +43,12 @@ export const NAV: NavGroup[] = [
   {
     title: 'Concepts',
     items: [
-      { id: 'dfp', label: 'Degradation-first', href: '/concepts/shrinking-quorum/' },
+      { id: 'dfp', label: 'Degradation-first', href: '/concepts/shrinking-quorum/#degradation-first' },
       { id: 'quorum', label: 'Shrinking quorum', href: '/concepts/shrinking-quorum/' },
       { id: 'gdi', label: 'Graceful Degradation Index', href: '/concepts/shrinking-quorum/#gdi' },
       { id: 'layers', label: 'Layers 0 to 5', href: '/concepts/architecture/' },
+      { id: 'prior', label: 'Prior art', href: '/concepts/prior-art/' },
+      { id: 'qual', label: 'Qualification path', href: '/concepts/qualification/' },
     ],
   },
   {
@@ -87,7 +96,7 @@ export const PAGES: DocPage[] = [
   {
     path: '/concepts/shrinking-quorum/',
     short: 'Shrinking quorum',
-    updated: '7 Oct 2026',
+    updated: '11 Oct 2026',
     file: 'src/pages/concepts/shrinking-quorum.astro',
   },
   {
@@ -96,10 +105,22 @@ export const PAGES: DocPage[] = [
     updated: '11 Oct 2026',
     file: 'src/pages/concepts/architecture.astro',
   },
+  {
+    path: '/concepts/prior-art/',
+    short: 'Prior art',
+    updated: '11 Oct 2026',
+    file: 'src/pages/concepts/prior-art.astro',
+  },
+  {
+    path: '/concepts/qualification/',
+    short: 'Qualification path',
+    updated: '11 Oct 2026',
+    file: 'src/pages/concepts/qualification.astro',
+  },
   {
     path: '/core/quorum-crate/',
     short: 'The quorum crate',
-    updated: '7 Oct 2026',
+    updated: '11 Oct 2026',
     source: 'quorum/src/lib.rs',
     file: 'src/pages/core/quorum-crate.astro',
   },

src/pages/concepts/architecture.astro

@@ -2,6 +2,7 @@
 import DocsLayout from '../../layouts/DocsLayout.astro';
 import DocsEnd from '../../components/DocsEnd.astro';
 import Breadcrumbs from '../../components/Breadcrumbs.astro';
+import { t } from '../../data/claims';
 
 const crumbs = [
   { label: 'Docs', href: '/' },
@@ -72,7 +73,7 @@ const crumbs = [
     </div>
 
     <h2 id="layers">Layers 0 to 5</h2>
-    <p>Only Layer 1 has code today. Layers 0 and 2 to 5 exist only in the whitepaper.</p>
+    <p>Only Layer 1 has code today. Layers 0 and 2 to 5 are not built. They exist only in the whitepaper.</p>
     <div class="tbl-box" tabindex="0">
       <table class="tbl">
         <thead>
@@ -88,7 +89,7 @@ const crumbs = [
           <tr>
             <td>0 · Survival kernel</td>
             <td class="m">§7</td>
-            <td>None</td>
+            <td>Not built</td>
             <td class="m">Paper</td>
             <td>None</td>
           </tr>
@@ -104,35 +105,36 @@ const crumbs = [
             </td>
             <td class="m">Prototype</td>
             <td>
-              Nine Kani proofs, 21 scenario checks and 37 F&#180; unit tests in CI, an F&#180; system test against the
-              demo, <a href="/core/bench/">bench</a> on general-purpose processors, Dusk
+              Nine Kani proofs, the scenario checks and 37 F&#180; unit tests in CI, a known-answer test coverage
+              campaign, an F&#180; system test against the demo, <a href="/core/bench/">bench</a> on general-purpose
+              processors, Dusk
             </td>
           </tr>
           <tr>
             <td>2 · Navigation and orientation</td>
             <td class="m">§9</td>
-            <td>None</td>
+            <td>Not built</td>
             <td class="m">Paper</td>
             <td>None</td>
           </tr>
           <tr>
             <td>3 · Science and knowledge triage</td>
             <td class="m">§10</td>
-            <td>None</td>
+            <td>Not built</td>
             <td class="m">Paper</td>
             <td>None</td>
           </tr>
           <tr>
             <td>4 · Communication</td>
             <td class="m">§11</td>
-            <td>None</td>
+            <td>Not built</td>
             <td class="m">Paper</td>
             <td>None</td>
           </tr>
           <tr>
             <td>5 · Bounded self-modification</td>
             <td class="m">§12</td>
-            <td>None</td>
+            <td>Not built</td>
             <td class="m">Paper</td>
             <td>None</td>
           </tr>
@@ -259,13 +261,13 @@ const crumbs = [
     <h2 id="products">Products and research</h2>
     <ul class="sig-list">
       <li>
-        <strong>Mru Flight</strong> runs Layer 1 on spacecraft. The F&#180; components <code>RedundancyManager</code>,{' '}
+        <strong>Mru Flight</strong> is Layer 1 for spacecraft. The F&#180; components <code>RedundancyManager</code>,{' '}
         <code>HealthRegistry</code> and <code>ReplicaHost</code> are built and tested: 37 unit tests, and a system test
-        that gives the demo&#39;s counts on the bench schedules. They have not run on flight hardware. A launcher for{' '}
-        <a href="/core/quorum-cli/#opssat">ESA&#39;s OPS-SAT</a> is in the repository.
+        against the demo&#39;s counts on the bench schedules. They have not run on flight hardware. A launcher for a{' '}
+        <a href="/core/quorum-cli/#opssat">proposed experiment on ESA&#39;s OPS-SAT</a> is in the repository.
       </li>
       <li>
-        <strong>Mru Field</strong> runs the same Layer 1 core on systems on Earth that are hard to reach. See{' '}
+        <strong>Mru Field</strong> is the same Layer 1 core for systems on Earth that are hard to reach. See{' '}
         <a href="https://mru.space/field/">Mru Field</a>.
       </li>
       <li>
@@ -301,10 +303,16 @@ const crumbs = [
         mru.space
       </li>
       <li>
-        <a href="/concepts/shrinking-quorum/">Shrinking quorum</a>: the Layer 1 rule and its guarantees
+        <a href="/concepts/shrinking-quorum/">Shrinking quorum</a>: the Layer 1 rule, what is proved and what is tested
+      </li>
+      <li>
+        <a href="/concepts/qualification/">Qualification path</a>: what exists against the NASA and ECSS software
+        standards
       </li>
       <li>
-        <a href="/simulation/dusk/">Dusk</a>: 10,000 missions, 1.34× the useful work of fixed TMR
+        <a href="/simulation/dusk/">Dusk</a>: {t('dusk.runs')} missions, {t('dusk.work_vs_tmr')} the useful work of
+        fixed TMR. This assumes no ground support after launch. The gain falls to {t('dusk.ground.never')} when support
+        never ends. See <a href="/simulation/dusk/#ground">Ground support</a>.
       </li>
     </ul>
     <DocsEnd />