LithosAnanke/docs/patent/os-template/OUTLINE.md

# Second provisional — outline (for approval before drafting)

Captain Bob, 2026-10-27. A completely new provisional, citing the SSM provisional (filed 2025-12-16,
docket SSM-001) where it builds on it. Target filing window 2026-12-01..14. Same form as the first:
LaTeX, `docs/patent/os-template/`, built like `ssm_RAJ_v1_patent_application.tex` (sections/02_field,
03_background, 04_summary, drawings, 06_detailed_description, 08_claims, abstract).

Not legal advice: claim wording, the priority question, and the prior-art search are for patent
counsel. Items marked **(my call)** are mine to check; **(open)** are his.

## Intent

Protect **the method that produces an operating system and its proofs together** — one method,
parameterised by the language, yielding a bootable image and a proof bundle bound to it, on a proven
frame that carries a self-tuning runtime proven not to change results; down to generated circuits
(FPGA, then ASIC: "proven silicon").

Who it serves (his words): embedded engineers, IoT hobbyists, academics, DARPA, medical-device and
avionics teams (where formal evidence is certification evidence: DO-178C/DO-333, IEC 62304), and AI
work using nodes as small neural nets; especially where an FPGA is available.

## Title (my call, draft)

**METHOD AND SYSTEM FOR PRODUCING AN OPERATING SYSTEM TOGETHER WITH ITS MACHINE-CHECKED PROOF,
PARAMETERISED BY PROGRAMMING LANGUAGE**. Docket **OST-001** (my call).

## Sections

**01 Title page** — title, inventor, provisional, cross-reference to SSM-001 (2025-12-16).

**02 Field** — formally verified computing systems; operating-system construction; hardware generated
from formal models; adaptive runtimes.

**03 Background** — what exists and what each lacks (from the 2026-10-27 prior-art search):
verified kernels (seL4, CertiKOS) prove one fixed OS, not hardware, not a template; verified stacks
(CLI Stack 1989; CakeML on Silver 2019) are one fixed language and one processor; verified hardware
generation (Kami, Kôika) has no OS or language layer; Isabelle-locale generic compilers parameterise
compilers, not systems; proof-carrying code attaches a proof to a program, not to a whole OS image;
self-adaptive systems (ActivFORMS) verify feedback loops statistically, never proving tuning leaves
results unchanged; verified systems avoid adaptive runtimes altogether. AI-generated OSes
(OSFoundry, 2026) are tested, not proven. The problem: each new OS, language or chip starts its
assurance from zero.

**04 Summary** — the three central elements, one paragraph each:
1. *Language as the parameter of the whole method* — a language-independent proven frame; a
   language plugs in by discharging stated obligations, mechanically where the tooling can, by hand
   where it cannot; either way the frame's theorems then hold for that OS.
2. *Image and proofs bound by content hash* — every capsule's ID is its content hash; the proof
   bundle names the hashes it was checked against; the booted system reports the same hashes (the
   POST parity line), so "this is the system that was proven" is checkable on the device.
3. *A self-tuning runtime proven not to change results* — the frame's adaptive runtime (SSM, cited)
   tunes itself while running, and the method proves no tuning changes what any program computes;
   every OS produced inherits both the tuning and the proof.
Then the supporting elements in a sentence each, among them (added 2026-10-28, Captain Bob):
*explicit epistemic status of every claim* -- at every level, a claim carries its evidence or says
plainly that it has none (stated / tested / proven).

**05 Drawings** (new figures; my call):
- FIG. 1 the method: language definition + frame -> obligations -> image + proof bundle (+ circuit).
- FIG. 2 the layers: proven machine (F18) / kernel contracts / blocks, ACL, identity / language
  instance (FORTH-79) / capsules — with where each named axiom sits.
- FIG. 3 the binding: capsule hashes in the bundle and on the booted device (a real POST excerpt).
- FIG. 4 the adaptive runtime beside execution: tuning state vs. execution state, the transparency
  theorem between them.
- FIG. 5 the hardware path: one model -> generated RTL -> FPGA fabric of nodes -> ASIC.
- FIG. 6 a second instance sketched (Lisp): which obligations it discharges, what it inherits.

**06 Detailed description**
- 6.1 The frame: the F18-style machine (instruction set, state, determinism); the kernel contracts;
  block storage; word-level ACL; identity (Zuse, Ed25519) — what each layer guarantees.
- 6.2 The language interface: the obligations (evaluator, dictionary/environment, error behaviour,
  resource bounds); discharged mechanically or by hand; what the frame then guarantees.
- 6.3 Producing the image: capsule build (mkcapsule), content addressing, the stick image (ESP,
  identity, Artemis).
- 6.4 Producing the proof bundle: theories, the axiom ledger (each axiom named, reasoned, and where
  it sits — hardware, compiler, crypto hardness), gaps listed separately from axioms.
- 6.5 Binding and checking: hashes in the bundle; POST on the device; parity across ISAs.
- 6.6 The adaptive runtime and its transparency proof (cite SSM-001 for the runtime itself).
- 6.7 Generated hardware: the machine's circuit from the proven model; FPGA (open-source flow);
  multi-node fabrics; ASIC.
- 6.8 Fabric uses: many nodes as small OSes or neural units.
- 6.9 Explicit epistemic status (added 2026-10-28, Captain Bob: "it ties with the sdk's concepts of
  prove it or say it's unproven explicitly"). One rule at three scales: *every claim carries its
  evidence, or says it has none.*
  - **The proofs:** the axiom ledger and the gap list (6.4) -- what cannot be proven, and why, is
    named rather than left silent.
  - **The method of construction:** a human ruling authority with an AI implementer under fixed
    rules -- a failing test before every change, every deviation a written ruling with its cost,
    acceptance evidence (boot logs, parity hashes) committed rather than summarised, acceptance on
    every increment.
  - **The software built for the system (the SDK's "book" capsule):** a capsule is a book of block
    pages -- natural-language statements of what it is and does, prompt pages that may regenerate
    the code pages after them, code pages, check pages, proof pages -- content-addressed, code pages
    and editions never removed; each promise shown as stated, tested or proven; the developer's
    English claims formalised (machine-assisted, the result translated back for the developer to
    confirm its meaning) and checked by a trusted proof checker; a fixed safety policy proven or
    enforced for every capsule.
  - The construction process thereby becomes the product's capsule format.

**07 Embodiments / working example** — LithosAnanke + StarForth v4 with FORTH-79 as the instance:
three ISAs booting with equal dict_hash, 538 POST cases, the 32-bit build (FPGA width), the stick;
DoE determinism (CV 0.000%); the Lisp sketch as a second embodiment.

**08 Claims (draft structure; counsel words them)**
- Independent 1 (method): providing a proven language-independent frame; receiving a language
  runtime and discharging the frame's obligations for it; producing a bootable image and a proof
  bundle; binding them by content hash.
- Independent 2 (system/runtime): the frame's adaptive runtime with a machine-checked proof that
  tuning does not alter computed results; inherited by every produced OS.
- Dependent: axiom ledger; explicit epistemic status of claims (stated / tested / proven) carried
  by the proof bundle and by each capsule; a capsule as a content-addressed book whose prompt pages
  regenerate its code pages and whose claims are formalised from natural language and checked; obligations discharged automatically or by hand; device-side hash
  check; circuit generated from the proven model (FPGA, ASIC); stack machine; multi-node fabric;
  nodes as neural units; FORTH-79 instance; second-language instance.

**Abstract** — ≤150 words.

## What must be true by filing (open)

A provisional must describe the method well enough to make and use it; it need not be finished.
What exists today: the frame running (v4 on three ISAs, POST, parity hashes), capsule hashing, the
v3 proof suite (52 theories, 2 axioms). Not yet: the v4 proof redo (moved up 2026-10-28: in the pause
after stick increment 4), the book capsule and its SDK (concept only), the language
locale, the transparency proof from the F18 model, generated RTL. **(open)** Which of these he wants
working, not just described, on filing day.

## Builder check (self-review, no subagent)

- Answered: form, location, central vs supporting, users, generated circuit, both obligation paths.
- My calls: title, docket OST-001, the six figures, the directory name.
- Open (his): what must be working by filing; the Lisp sketch's depth.