From f5866d39cc39ae63cfd699368b2e1898619e4510 Mon Sep 17 00:00:00 2001 From: rajames Date: Wed, 28 Oct 2026 09:31:19 -0400 Subject: [PATCH] docs(patent): the second provisional's outline -- the OS-and-proofs method, with explicit epistemic status The outline for approval before drafting (target filing 2026-12-01..14, citing SSM-001): the method that produces an operating system and its machine-checked proofs together, parameterised by language; image and proofs bound by content hash; the self-tuning runtime proven not to change results. Added 2026-10-28: explicit epistemic status of every claim -- proofs, the method of construction, and the SDK's book capsule (6.9, and the claims' structure). Co-Authored-By: Claude Opus 5.5 --- docs/patent/os-template/OUTLINE.md | 131 +++++++++++++++++++++++++++++ 1 file changed, 131 insertions(+) create mode 100644 docs/patent/os-template/OUTLINE.md diff --git a/docs/patent/os-template/OUTLINE.md b/docs/patent/os-template/OUTLINE.md new file mode 100644 index 00000000..502306a7 --- /dev/null +++ b/docs/patent/os-template/OUTLINE.md @@ -0,0 +1,131 @@ +# 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.