AbstractTo our knowledge, Phosphoric is the first public working prototype of a forensic-primacydeterministic computing substrate spanning language, compiler, kernel, and operating-system layers: forensic evidence is not reconstructed from logs after execution, but emittedas typed residual records by the running substrate, chained into a PFI0 case file, andreplayed through a closed deterministic verdict table. Phosphoric is a from-scratch systems stack for single-task edge devices. No Rust, no LLVM, no external linker, no libc, no POSIX surface — everything below the application is in-tree. The stack is four pieces. Phosphoric is the language: a closed v0 grammar with affine capabilities, fixed-capacitycollections, a six-element runtime effect alphabet, and per-function effect declarations. ‘noₛtd‘, ‘noₐlloc‘, ‘noᵤnsafe‘, no FFI. pcc is the self-hosted compiler: parses Phosphoric source and emits PE/COFF EFI directly, no assembler, no linker, no third-party codegen. The bootstrap reduces to a small ASMstub whose hash is pinned and whose source-to-ASM correspondence is byte-equal verified. Ember is the trusted nucleus — 330 LOC on x86₆4, per-arch ceilings 100–800 — owningCPU primitives, MMIO, and port I/O behind line-audited ‘trusted¡ blocks. PhosphorOS is the kernel above Ember: fixed-capacity tables (64 tasks, 128 channels, 256capability slots), generation-tagged handles, cooperative scheduling, one manifest-sealedtask per device. The closed grammar and per-image manifest force the authority graph — capabilities, IPCchannels, MMIO ranges, effects, budgets — to be enumerated at build time, hashed into a‘. pmanifest‘ certificate bundle, and cross-checked at boot and at every runtime authoritytransition. The kernel emits seven typed residual records at those transitions; a chain-hash mixer folds each event into a deterministic stream that an off-device court re-derivesindependently. Single-purpose edge devices — industrial control terminals, defense sensor heads, medicalinstrument controllers, classified-environment appliances, voting machines, HSM-class roots-of-trust, mission-critical field hardware — already produce dense observable streams through syscalltraces, kernel logs, hardware telemetry, and exception records. Forensic action, however, remainsdominated by post-incident log analysis that reconstructs structure heuristically from bytestreams that were never typed for forensic interpretation in the first place. This paper studiesthe Phosphoric substrate (language + Ember nucleus + PhosphorOS runtime) as a DSFB-nativeexecution layer that emits typed residuals at every authority boundary, by construction. It does not propose a replacement for general-purpose operating systems, a competi-tor to seL4, Tock, or MirageOS, or a new formal-methods methodology. Instead, it mapsthe seven DSFB residual signs — capgraphdelta, ipcᵣoutedelta, budgetₚressure, effectₜrace, mmioₜouch, taskₜransition, and bootcheck — onto the seven authority-boundary kinds the language and kernel can structurally emit, and shows that the emissioncontract is enforced at compile time via Phosphoric’s affine capability/type discipline, the closedv0 effect alphabet, the trusted-profile partition, and the per-image task manifest. The paper makes a bounded claim. It shows how a closed-grammar language, a 100–350 LOCtrusted nucleus, and a fixed-capacity capability runtime can be composed so that observedruntime behavior is a structural subset of the build-time authority graph by construction —not by runtime monitoring after the fact. It does not prove standards compliance, completedcertification, machine-checked refinement (in the seL4 sense), or universal superiority overexisting formal-methods stacks. It does not claim Phosphoric is more secure than seL4; it claimsit is more task-sealed on a different axis. The empirical evidence is the Phosphoric v0. 3 razor-court emission release: a Phosphoric-source-derived UEFI bootable which, under QEMU/OVMF, prints the DSFB primary theorem, emits three typed runtime residual records (R7 bootcheck, R6 taskₑnter, R6 taskₑxit), packages the captured stream into a chain-anchored PFI0 case file, and replays to a byte-stableNODRIFT verdict. The court independently re-derives each chainₕash step and rejects drift. The demonstration establishes the admitted v0. 3 razor case; it does not claim production siliconvalidation, general OS completeness, or machine-checked refinement.
Riaan De Beer (Mon,) studied this question.