leanos

KO | EN

gitlite — search

#nextjs #codex #tailwindcss #agent #csharp #react-native #monitoring #nlp #svg #generative-ai

(★ 9)

experimental LeanOS formally verified OS

File Explorer

ZIP Download

Showing a partial file list — download the zip above to see everything.

- - ci-image.yml
  - ci.yml
  - pages.yml
  - release.yml
  - ruleset-audit.yml
  - toolchain-compatibility.yml
- main-ruleset-policy.json
- leanos-social-preview.png
- acpi-dsdt-address.h
- boot.S
- grub-double-fault.cfg
- grub-nmi-cpl3.cfg
- grub.cfg
- kernel.c
- linker.ld
- pci-af-observation.h
- pci-capabilities.h
- pci-command-executor.h
- pci-config-read.h
- pci-config-read.S
- pci-enumeration.h
- pci-express-observation.h
- pci-power-observation.h
- peer-pke-fixture.S
- qotom-ahci-bme.h
- qotom-ahci-capabilities.h
- qotom-ahci-interrupts.h
- qotom-ahci-port.h
- qotom-broadcom-d3.h
- qotom-ecam-read.h
- qotom-ehci-bme.h
- qotom-ehci-capabilities.h
- qotom-ehci-handoff.h
- qotom-ehci-legacy.h
- qotom-ehci-operational.h
- qotom-ehci-smi.h
- qotom-graphics-bme.h
- qotom-graphics-state.h
- qotom-hda-bme.h
- qotom-hda-observation.h
- qotom-hda-state.h
- qotom-native-inventory.h
- qotom-pci-final-admission.h
- qotom-pcie-pending.h
- qotom-realtek-bme.h
- qotom-realtek-route.h
- qotom-realtek-state.h
- qotom-rootport-bme.h
- qotom-txe-bme.h
- qotom-txe-status.h
- qotom-xhci-bme.h
- qotom-xhci-capabilities.h
- qotom-xhci-handoff.h
- qotom-xhci-legacy.h
- qotom-xhci-operational.h
- qotom-xhci-smi.h
- Dockerfile
- manifest-v1.json
- provisional-source-build-evidence-v1.json
- README.md
- - 0001-phase-1-scope-threat-model-and-tcb.md
  - 0002-freestanding-lean-boundary.md
  - 0003-ring3-syscall-fault-slice.md
  - 0004-two-subject-ipc-slice.md
  - 0005-one-shot-timer-preemption.md
  - 0006-smap-user-copy-window.md
  - 0007-double-fault-ist.md
  - 0008-bounded-resumable-preemption.md
  - 0009-blocking-ipc-boot.md
  - 0010-defer-fork.md
  - 0011-qemu-wasm-feasibility.md
  - 0012-frame-budget-exhaustion-and-reuse.md
  - 0013-kvm-on-host-evidence.md
  - 0014-toolchain-compatibility-profiles.md
  - 0015-guarded-privilege-entry-stack.md
  - 0016-physical-rejection-evidence.md
  - 0017-qotom-kernel-copy-roots.md
  - 0018-qotom-pci-initial-trust-contract.md
  - 0019-typed-platform-admission.md
- bare-metal-observation.schema.json
- bare-metal-rejection-capture.md
- blocking-ipc.md
- boot-allocation.md
- boot-image.md
- boot-memory-map.md
- boot-reservations.md
- browser-boot.md
- browser-demo-licenses.md
- capability-handles.md
- capability-model.md
- capability-transfer.md
- direct-port-io.md
- dma-quarantine.md
- early-text-console.md
- endpoint-ipc.md
- extended-state-denial.md
- fail-stop.md
- fault-dispatch.md
- firmware-handoff-corpus.md
- frame-allocator.md
- frame-budgets.md
- frame-scrubbing.md
- interrupt-model.md
- iommu-confinement.md
- j1900-entry-review.md
- lifetime-identity.md
- memory-lifecycle.md
- model-oracle.md
- observation-model.md
- page-fault-snapshot.md
- pci-capability-observation.md
- pci-command-executor.md
- pci-config-read.md
- pci-enumeration.md
- pci-header-observation.md
- pci-header-scalar.md
- platform-admission-profiles.md
- privilege-entry-control.md
- qotom-ahci-observation.md
- qotom-apic-lvt-observation.md
- qotom-blocking-ipc-integration.md
- qotom-boot-recovery-lab.md
- qotom-broadcom-d3.md
- qotom-bsp-consumer.md
- qotom-bsp-lab.md
- qotom-bsp-production-boundary.md
- qotom-bsp-topology-candidate.md
- qotom-ecam-read-candidate.md
- qotom-ehci-ownership.md
- qotom-exception-integration.md
- qotom-graphics-bme.md
- qotom-graphics-state.md
- qotom-hardware-bringup.md
- qotom-hda-bme.md
- qotom-hda-observation.md
- qotom-hda-state.md
- qotom-lpc-command-constraint.md
- qotom-madt-consumer-review.md
- qotom-madt-scalar-stream.md
- qotom-msr-write-audit.md
- qotom-native-device-control.md
- qotom-native-fields.md
- qotom-native-inventory-image.md
- qotom-native-inventory.md
- qotom-pci-final-admission.md
- qotom-pci-inventory.md
- qotom-pci-selector-rejection.md
- qotom-pcie-device-observation.md
- qotom-pcie-pending.md
- qotom-quarantine-observation.md
- qotom-quarantine-transition.md
- qotom-realtek-bme.md
- qotom-realtek-state.md
- qotom-recovery-acceptance.md
- qotom-reset-header-observation.md
- qotom-rootport-bme.md
- qotom-txe-bme.md
- qotom-txe-status.md
- qotom-watchdog-lab.md
- qotom-xhci-ownership.md
- release-notes.md
- scheduled-observation.md
- scheduler.md
- security-claims.md
- subject-lifecycle.md
- syscall-model.md
- tlb-model.md
- toolchain-compatibility.md
- user-copy.md
- virtual-mapping.md
- vtd-boot-plan.md
- x86-page-tables.md
- - binding-replay.c
  - binding-test.c
  - binding.h
  - binding.md
  - construct-fixture.c
  - construct-replay.c
  - construct-test.c
  - construct.h
  - construct.md
  - entry.S
  - fixture.ld
  - fixture.S
  - operands-fixture.c
  - operands-replay.c
  - operands-test.c
  - operands.h
  - operands.md
  - reload.S
  - return-fixture.S
  - return.md
  - return.S
  - transfer-fixture.inc
  - transfer.S
- - fixture.c
  - fixture.ld
  - fixture.S
- - Boundary.lean
  - entry.S
  - primitives.c
- - Hosted.lean
- - fixture.ld
  - fixture.S
- - fixture.c
  - fixture.ld
  - fixture.S
- - executing-apic-id.txt
  - memmap.tsv
  - provenance.json
- - executing-apic-id.txt
  - memmap.tsv
  - provenance.json
- - executing-apic-id.txt
  - memmap.tsv
  - provenance.json
- - executing-apic-id.txt
  - memmap.tsv
  - provenance.json
- - executing-apic-id.txt
  - memmap.tsv
  - provenance.json
- - executing-apic-id.txt
  - memmap.tsv
  - provenance.json
- - acpi-root-address.txt
  - cpu0-sample.txt
  - efi-map.bin
  - executing-apic-id.txt
  - memmap.tsv
  - provenance.json
- manifest.json
- qotom-native-handoff.json
- qotom-native-root.json
- - .gitattributes
  - capture-cpuid.c
  - capture-pci.py
  - chain-sentinel.S
  - FREEBSD-FIRMWARE.md
  - grub-qotom-watchdog-window.cfg
  - grub-qotom-watchdog.cfg
  - grub-qotom.cfg.in
  - PCI-CAPTURE.md
- .gitattributes
- bundle.schema.json
- LeanOS__BlockingIPC.md
- LeanOS__BlockingIPCContext.md
- LeanOS__BootAllocation.md
- LeanOS__BootInterruptPhase.md
- LeanOS__BootMemoryMap.md
- LeanOS__BootMemoryMapDecoder.md
- LeanOS__BootMemoryMapDecoderABI.md
- LeanOS__BootMemoryMapFullProjectionABI.md
- LeanOS__BootMemoryMapScalarRichEquivalence.md
- LeanOS__BootMemoryMapStreamAuthority.md
- LeanOS__BootMemoryMapStreaming.md
- LeanOS__BootMemoryMapStreamPipeline.md
- LeanOS__BootPageTablePlan.md
- LeanOS__BootReservation.md
- LeanOS__BootTextConsole.md
- LeanOS__BootTopology.md
- LeanOS__BoundaryVocabulary.md
- LeanOS__BoundedLifecycle.md
- LeanOS__Capability.md
- LeanOS__CapabilityHandle.md
- LeanOS__CapabilityReuse.md
- LeanOS__CapabilityTransfer.md
- LeanOS__CompositeDispatcher.md
- LeanOS__CompositeFootprint.md
- LeanOS__DirectPortContainment.md
- LeanOS__DirectPortIO.md
- LeanOS__DMAQuarantine.md
- LeanOS__DMAQuarantineCorpus.md
- LeanOS__EndpointIPC.md
- LeanOS__Example.md
- LeanOS__ExtendedState.md
- LeanOS__FailStop.md
- LeanOS__FaultDispatch.md
- LeanOS__FrameAllocator.md
- LeanOS__FrameBudget.md
- LeanOS__FrameBudgetScenario.md
- LeanOS__FrameScrub.md
- LeanOS__Interrupt.md
- LeanOS__InterruptEntry.md
- LeanOS__InvalidationPublication.md
- LeanOS__IOMMU.md
- LeanOS__IOTLB.md
- LeanOS__IPCSyscall.md
- LeanOS__J1900CpuControlPolicy.md
- LeanOS__J1900CpuProfile.md
- LeanOS__J1900EntryControl.md
- LeanOS__J1900MsrReadback.md
- LeanOS__KernelRootPublication.md
- LeanOS__KernelRootReturn.md
- LeanOS__KernelTransition.md
- LeanOS__KernelUserRoot.md
- LeanOS__LifetimeIssuer.md
- LeanOS__MemoryLifecycle.md
- LeanOS__Observation.md
- LeanOS__Oracle.md
- LeanOS__PCIHeaderObservation.md
- LeanOS__PlatformAdmission.md
- LeanOS__Preemption.md
- LeanOS__PrivilegeEntryControl.md
- LeanOS__PrivilegeEntryStack.md
- LeanOS__QotomBlockingIPCIntegration.md
- LeanOS__QotomBootstrapABI.md
- LeanOS__QotomBspTopology.md
- LeanOS__QotomCopyRootPublication.md
- LeanOS__QotomEntryIntegration.md
- LeanOS__QotomMadtStream.md
- LeanOS__QotomMadtStreamRun.md
- LeanOS__QotomNativePCIFields.md
- LeanOS__QotomNativePCIInventory.md
- LeanOS__QotomNativePCISnapshot.md
- LeanOS__QotomNoSmapControl.md
- LeanOS__QotomPCIFinalAdmission.md
- LeanOS__QotomPCIInventory.md
- LeanOS__QotomPCIQuarantineObservation.md
- LeanOS__QotomPCIQuarantineTransition.md
- LeanOS__ResumablePreemption.md
- LeanOS__ScheduledObservation.md
- LeanOS__Scheduler.md
- LeanOS__SecurityClaims.md
- LeanOS__SerialProtocol.md
- LeanOS__StaleTranslation.md
- LeanOS__SubjectLifecycle.md
- LeanOS__Syscall.md
- LeanOS__TLB.md
- LeanOS__UserCopy.md
- LeanOS__UserCopyAliases.md
- LeanOS__UserCopyBinding.md
- LeanOS__UserCopyOperands.md
- LeanOS__UserCopyPrefix.md
- LeanOS__UserCopyTransaction.md
- LeanOS__UserCopyWindow.md
- LeanOS__UserFaultContainmentVocabulary.md
- LeanOS__VirtualMapping.md
- LeanOS__VTdBootPlan.md
- LeanOS__X86PageTable.md
- manifest.json
- - BootMemory.lean
  - BootPhase.lean
  - BootPlans.lean
  - BootTopology.lean
  - DirectPort.lean
  - DMAQuarantine.lean
  - Example.lean
  - FrameBudget.lean
  - IOMMUConfinement.lean
  - NMIFrame.lean
  - NMIHalt.lean
  - NMIManifest.lean
  - PageFaultAgreement.lean
  - PageFaultError.lean
  - PageFaultProvenance.lean
  - SecurityClaims.lean
  - SharedContainment.lean
  - StaleTranslation.lean
  - UserFaultClass.lean
  - VTdBootPlan.lean
  - WrappingIssuerReuse.lean
- BlockingIPC.lean
- BlockingIPCContext.lean
- BootAllocation.lean
- BootInterruptPhase.lean
- BootMemoryMap.lean
- BootMemoryMapDecoder.lean
- BootMemoryMapDecoderABI.lean
- BootMemoryMapFullProjectionABI.lean
- BootMemoryMapScalarRichEquivalence.lean
- BootMemoryMapStreamAuthority.lean
- BootMemoryMapStreaming.lean
- BootMemoryMapStreamPipeline.lean
- BootPageTablePlan.lean
- BootPageTablePlanGenerator.lean
- BootReservation.lean
- BootTextConsole.lean
- BootTopology.lean
- BoundaryABIGenerator.lean
- BoundaryVocabulary.lean
- BoundedLifecycle.lean
- Capability.lean
- CapabilityHandle.lean
- CapabilityReuse.lean
- CapabilityTransfer.lean
- CompositeDispatcher.lean
- CompositeFootprint.lean
- DirectPortContainment.lean
- DirectPortIO.lean
- DMAQuarantine.lean
- DMAQuarantineCorpus.lean
- EndpointIPC.lean
- Example.lean
- ExtendedState.lean
- FailStop.lean
- FaultDispatch.lean
- FrameAllocator.lean
- FrameBudget.lean
- FrameBudgetScenario.lean
- FrameScrub.lean
- Interrupt.lean
- InterruptEntry.lean
- InvalidationPublication.lean
- IOMMU.lean
- IOTLB.lean
- IPCSyscall.lean
- J1900CpuControlPolicy.lean
- J1900CpuProfile.lean
- J1900EntryControl.lean
- J1900MsrReadback.lean
- KernelRootPublication.lean
- KernelRootReturn.lean
- KernelTransition.lean
- KernelUserRoot.lean
- LifetimeIssuer.lean
- MemoryLifecycle.lean
- NegativeFixtures.lean
- Observation.lean
- Oracle.lean
- PCIHeaderObservation.lean
- PlatformAdmission.lean
- Preemption.lean
- PrivilegeEntryControl.lean
- PrivilegeEntryStack.lean
- QotomBlockingIPCIntegration.lean
- QotomBootstrapABI.lean
- QotomBspTopology.lean
- QotomCopyRootPublication.lean
- QotomEntryIntegration.lean
- QotomMadtStream.lean
- QotomMadtStreamRun.lean
- QotomNativePCIFields.lean
- QotomNativePCIInventory.lean
- QotomNativePCISnapshot.lean
- QotomNoSmapControl.lean
- QotomPCIFinalAdmission.lean
- QotomPCIInventory.lean
- QotomPCIQuarantineObservation.lean
- QotomPCIQuarantineTransition.lean
- ResumableContext.lean
- ResumablePreemption.lean
- ScheduledObservation.lean
- Scheduler.lean
- SecurityClaims.lean
- SerialProtocol.lean
- StaleTranslation.lean
- SubjectLifecycle.lean
- Syscall.lean
- TLB.lean
- UserCopy.lean
- UserCopyAliases.lean
- UserCopyBinding.lean
- UserCopyOperands.lean
- UserCopyPrefix.lean
- UserCopyTransaction.lean
- UserCopyWindow.lean
- UserFaultContainmentVocabulary.lean
- VirtualMapping.lean
- VTdBootPlan.lean
- VTdBootPlanGenerator.lean
- X86PageTable.lean
.gitignore
.markdownlint-cli2.jsonc
Containerfile.ci
INVARIANTS.identities.json
INVARIANTS.md
LeanOS.lean
LICENSE
README.md

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Version

File

Showing a partial file list.

Link

Example

# Project Badges

LeanOS — a formally modeled operating-system kernel

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

LeanOS is an experiment in building a small operating-system kernel whose
implementation, executable specification, and machine-checked proofs evolve
together in Lean 4.

**[▶ Boot LeanOS in your browser](https://rudi-cilibrasi.github.io/leanos/)** —
watch the unchanged canonical ISO boot live in a pinned WebAssembly QEMU, from
firmware through the versioned protocol to `LEANOS/10 FINAL status=PASS` and
guest debug-exit 33. Needs a desktop browser with cross-origin isolation;
first load downloads a ~40 MB runtime.
[How the demo is built and what it does and does not prove](docs/browser-boot.md).

**[📖 What LeanOS provably guarantees, in plain English](INVARIANTS.md)** — a
generated, machine-checked index that explains every Lean theorem in the
repository (all of them, and only them) for readers without a formal-methods
background.

The project is an **experimental research prototype**, not a verified operating
system. It now builds bootable x86-64 images, exercises several deterministic
machine scenarios under QEMU, and checks a growing set of Lean models and
theorems. Those are different kinds of evidence: the theorems apply to the
models, while QEMU tests selected compiled integration paths.

## Current status

The evidence paths meet in the repository, but they do not carry the same
claim. In particular, the compiled path crosses a trusted, unproved boundary:

```mermaid
flowchart TB
 M["Lean executable models"] --> T["Lean theorem statements and proof source"]
 T --> E["Lean elaborator"]
 E --> R["Elaborated proof terms"]
 R --> K["Lean kernel proof-term checker"]
 K --> P["Lean-proved model properties"]

M --> G
 subgraph TCB["Trusted / unproved implementation and execution boundary"]
 direction TB
 G["Lean code generation and generated C"]
 B["Runtime shim, handwritten C/assembly, compiler, linker, and boot chain"]
 Q["QEMU/TCG and assumed x86-64/device semantics"]
 G --> B --> Q
 end

Q --> O["QEMU-tested finite scenario observations"]
 P -. "no refinement theorem" .-> O

classDef proved fill:#d5f5e3,stroke:#18794e,color:#111
    classDef tested fill:#dbeafe,stroke:#2563eb,color:#111
    classDef trusted fill:#fff3cd,stroke:#9a6700,color:#111
    class P proved
    class O tested
    class K,G,B,Q trusted
```

The dashed edge marks the missing model-to-binary refinement theorem; it does
not turn the QEMU observations into proof. Trusted coloring covers both the
Lean kernel assumed to check elaborated proof terms soundly and the unproved
implementation/execution path whose correctness is assumed when interpreting
the tested observations. The elaborator constructs proof terms, but the kernel
rechecks those terms rather than trusting the elaborator's result directly.

There is one explicitly inventoried exception to a kernel-reduction-only proof
path. For approved bounded computations, `native_decide` compiles and runs a
`Decidable` instance with Lean's native evaluator and records the result through
`Lean.ofReduceBool`. The kernel checks the resulting term but does not replay the
native computation, so those declarations also trust the Lean compiler,
generated native code, evaluator/interpreter, and selected `@[implemented_by]`
definitions. The policy and module inventory are part of
[ADR 0001](docs/adr/0001-phase-1-scope-threat-model-and-tcb.md#native-evaluation-proof-policy).

### QEMU-tested behavior

The CI image boots headlessly on a single emulated x86-64 `q35` CPU under TCG.
Success requires an exact serial transcript, a guest debug-exit signal, and
completion within a fixed timeout; merely reaching the kernel or printing a
partial log does not pass. The executable scenarios currently include:

- the default two-subject, two-address-space blocking-IPC path, from B blocking
  on an empty endpoint through A's send/wake to exact delivery back to B;
- an independent admitted-frame-budget path in which A reaches its one-frame
  limit without starving B, checked termination restores one unit, and an
  allocator-selected physical frame is scrubbed and reused through a
  generated ring-3 mapping before B receives a fresh lifetime;
- a bounded preemption path with two PIT interrupts, separate saved contexts,
  CR3 changes, a switch from A to B, and resumption of A's original frame;
- an independent user-fault containment path that terminates A through the
  typed composite dispatch contract and resumes B in B's owned address space;
- boot-time memory-map validation, reservation, frame scrubbing and publication,
  live page-table checks, WP/SMEP/SMAP probes, and bounded user-copy checks;
- a dedicated double-fault IST fail-stop probe and a mapped-guard negative;
- two early-IDT fail-stop probes: a real pre-paging `ud2` that vector 6 must
  carry through the kernel-owned 32-bit bootstrap IDT to its pinned terminal
  stub, and a QMP-injected NMI delivered after an exact early-only readiness
  record while the 64-bit bootstrap IDT is live but the runtime IDT is still
  unpublished;
- a controlled fast-entry machine-state relaxation that must be caught by the
  live outbound MSR read-back before CPL3; and
- a bounded suite of deliberately corrupted user-return images that must fail
  with their expected typed rejection before reaching CPL3.

Before the main machine path, the normal images also replay the same bounded
389-vector [model-oracle corpus](docs/model-oracle.md) evaluated by Lean and by
hosted generated C. These finite QEMU runs provide reproducible integration
evidence for the named scenarios. They are not exhaustive tests, hardware
qualification, or proofs that the binary refines the Lean models.

### Opt-in physical-machine evidence

A [Qotom J1900 capture](docs/qotom-hardware-bringup.md) records the unchanged
image booting from USB and rejecting the physical PCI identity before CPL3.
The separate `hardware` tier requires an exact serial rejection and bounded
post-terminal silence; it is not hardware admission or a required CI run.

### Lean-proved properties

The default Lake target builds the kernel reference models and their
machine-checked proofs. The proved surface includes, among other properties,
deterministic kernel transitions, invariant and well-formedness preservation,
capability-authority provenance, exclusive frame ownership, page-table
separation, syscall confinement, fail-stop absorption, user-return confinement,
and finite scheduled observer isolation. The
[security claim index](docs/security-claims.md) is the canonical summary of
advertised theorem statements, assumptions, and exclusions.

Every such result is a theorem about its named Lean state, transition, and
assumptions. Unless an explicit refinement theorem is added, it says nothing by
itself about generated C, handwritten boot code, QEMU execution, or physical
hardware.

### Proof and evidence enforcement

`./scripts/check.sh` builds every default Lean module with warnings as errors,
checks the security-claim index against independently typed contract theorems,
replays the generated-C oracle, runs boundary and host-harness regressions, and
requires deliberately invalid or weakened proof fixtures to remain rejected.
It also rejects `sorry`, `admit`, and unapproved `axiom`, `constant`, `unsafe`,
`extern`, or FFI declarations in project Lean sources. CI runs that gate before
building and booting the images, then retains the image, ELF, map, generated
page-table plans, tool versions, and serial evidence for inspection.

These checks protect the repository's stated proof discipline; they do not
verify Lean's kernel, the code generator, the C compiler, or the resulting
machine code.

### Trusted and tested boundaries

The current trusted computing base still includes handwritten assembly and C,
the restricted Lean runtime shim, Lean code generation and generated C, the C
compiler and binutils, linker scripts, GRUB, SeaBIOS, QEMU/TCG, host-side
evidence scripts, and the assumed x86-64 and device semantics. The boot scenarios
test only the fixed single-core paths and adversarial cases documented by their
ADRs. General concurrency, DMA outside the finite q35 quarantine and static
IOMMU models, device-read confidentiality outside explicitly authorized model
views, timing and covert channels, arbitrary hardware, arbitrary faults, and
full implementation refinement remain outside
the current claims. [ADR 0001](docs/adr/0001-phase-1-scope-threat-model-and-tcb.md) defines
the evidence vocabulary and baseline boundary; later ADRs record each addition.

## Why LeanOS?

Projects such as seL4 show the value of connecting a kernel implementation to a
formal model. LeanOS explores how much of that connection can live in one Lean
4 codebase:

- executable models beside the theorems that constrain them;
- small kernel interfaces with explicit preconditions and postconditions;
- proof-carrying changes checked on every pull request;
- emulator tests that connect abstract claims to a bootable artifact; and
- a documented trusted computing base (TCB), including every unverified bridge
  between Lean, generated code, the runtime, the linker, and hardware.

This is a research project, not a claim that writing code in Lean automatically
makes an operating system verified. Compiler correctness, runtime behavior,
foreign code, boot code, device models, and hardware assumptions all matter.
Making those boundaries visible is part of the work.

## Project principles

1. **State claims precisely.** Every advertised guarantee must name its model,
   assumptions, proof, and executable boundary.
2. **Keep the TCB small and visible.** Unverified assembly, C, firmware, tools,
   and runtime components are tracked rather than hidden behind “verified.”
3. **Prove vertical slices.** Prefer a tiny path from specification to booted
   behavior over a broad collection of disconnected theorems.
4. **Test the boundary.** Proofs cover models; QEMU and hardware tests cover the
   integration points where those models meet reality.
5. **Reproduce everything.** Pin toolchains and make local and CI commands use
   the same scripts.

## Boot and model progress

The first vertical-slice milestone is now implemented as a deterministic,
headless QEMU boot that:

1. loads a versioned x86-64 image;
2. initializes the minimum required runtime;
3. prints a known message over the serial console;
4. exercises one Lean-specified kernel state transition;
5. exits QEMU with a machine-readable success code; and
6. is built, proved, booted, and checked by GitHub Actions.

The selected boundary uses a minimal assembly/C loader around restricted,
allocation-free generated C from Lean. That bridge is deliberately small and
tested, but remains part of the TCB rather than a proved refinement layer.

The target platform, Phase 1 threat model, proof vocabulary, allowed milestone
claims, and initial trusted computing base are fixed in
[ADR 0001](docs/adr/0001-phase-1-scope-threat-model-and-tcb.md). In particular,
successful compilation or QEMU execution is integration evidence, not proof of
the generated binary or boot chain.

[ADR 0002](docs/adr/0002-freestanding-lean-boundary.md) selects a restricted,
allocation-free generated-C export for the first Lean/boot boundary and records
the reproducible experiments and trusted assumptions behind that decision.

The Phase 1 image can be built with `./scripts/build-image.sh` and exercised
headlessly with `./scripts/run-image.sh`; the stable protocol, pinned reference
tools, debug artifacts, and added trusted boundary are documented in
[the boot-image guide](docs/boot-image.md).

The same unchanged image also boots in a browser: the
[in-browser boot compatibility harness](docs/browser-boot.md) runs the canonical
ISO in a pinned, unforked qemu-wasm WebAssembly runtime and requires the
identical versioned serial protocol and debug-exit status through the native
`scripts/run-image.sh` acceptance path. It is compatibility evidence at a
trusted boundary, not a proof of the browser or emulator.

**[▶ Boot LeanOS in your browser](https://rudi-cilibrasi.github.io/leanos/)** —
the unchanged canonical ISO running live in a pinned WebAssembly QEMU. First
load downloads a ~40&nbsp;MB runtime and needs a desktop browser with
cross-origin isolation (`SharedArrayBuffer`); the page shows the boot protocol
until `LEANOS/10 FINAL status=PASS` and a guest debug-exit of 33. The deployed
site is staged from source-verified pinned assets by
[`scripts/stage-browser-demo.sh`](scripts/stage-browser-demo.sh) and its
[third-party licenses](docs/browser-demo-licenses.md) are inventoried; it is
emulator-tested integration evidence, not a proof of LeanOS, the browser, or the
emulator.

The first Phase 2 executable boundary boots one deliberately tiny ring-3
subject through an `int 0x80` gate, binds its calls to kernel-selected context,
and contains one expected user page fault. Its assumptions and evidence are
recorded in [ADR 0003](docs/adr/0003-ring3-syscall-fault-slice.md).

The two-subject integration slice extends that boundary with separate page
tables and a fixed cooperative handoff through one directional endpoint. Its
tested behavior and unproved machine boundary are recorded in
[ADR 0004](docs/adr/0004-two-subject-ipc-slice.md).

The [one-shot timer slice](docs/adr/0005-one-shot-timer-preemption.md) uses a
documented PIT interrupt to preempt a non-yielding subject and tests the
scheduler-derived caller/address-space switch to the second subject.

The [bounded SMAP copy slice](docs/adr/0006-smap-user-copy-window.md) composes
whole-range user-copy validation with an explicit AC window and exercises one
fixed boot syscall. Its Lean results are model-level; the assembly window and
machine behavior remain trusted and integration-tested.

The first executable model is `LeanOS.KernelTransition.transition`, with
machine-checked determinism, invariant-preservation, and rejection-stability
theorems in
[`LeanOS/KernelTransition.lean`](LeanOS/KernelTransition.lean). The boot-slice
[issue #6](https://github.com/rudi-cilibrasi/leanos/issues/6) must invoke the
exact fixed-width export `LeanOS.KernelTransition.bootTransition` (C symbol
`leanos_boot_transition`) and test its encoded accepted and rejected results.
That adapter is proved to agree with the model for well-formed encoded states;
the generated code and boot boundary remain trusted rather than proved.

The first capability-security reference model is documented in
[`docs/capability-model.md`](docs/capability-model.md). Its Lean theorems prove
well-formedness preservation, state-preserving rejection, and authority
provenance for a minimal copy/revoke operation set. These are model-level
properties, not claims about information flow, covert channels, concurrency,
object lifetimes, generated code, or a kernel binary.

Holder-visible [generation-bound capability handles](docs/capability-handles.md)
pair each bounded subject-local slot with its never-reused capability identity,
so clearing or replacing a slot cannot make an old handle authorize the new
occupant.

The finite [user extended-state denial model](docs/extended-state-denial.md)
requires an explicit fail-closed CR0/CR4 policy before modeled user return and
confines typed x87/MMX/SIMD denial to the authoritative current subject. Its
cleanup transition reuses the scheduler, lifecycle, mapping/TLB, and resumable
context state, then selects only a kernel-owned peer context or typed idle.
Machine exception delivery and cleanup/restore remain trusted integration work
rather than theorem claims.

The finite [PCI DMA-quarantine model](docs/dma-quarantine.md) validates a
versioned q35 manifest and proves, under an explicit device-control contract,
that a named present unassigned function cannot change physical memory,
allocator ownership, page-table or kernel-owned frames, kernel state, or any
subject-visible bytes. This is an integrity claim only: it does not constrain
device reads or prove confidentiality, IOMMU isolation, or refinement from the
Lean snapshot to the implementation. The repository's mandatory runners use
one explicit `-nodefaults` construction with a pinned VGA BDF and boot-CD
attachment. The guest exhaustively checks that manifest after firmware, clears
bus mastering on every present function, and reads each Command register back
before CPL3. Every later CPL3 return re-enumerates the manifest and requires
the complete live Command words to match that accepted boot observation.
PCI enumeration and Command-register semantics, QEMU/device
obedience, the handwritten C adapter, and final-binary correspondence remain
trusted/tested boundaries rather than proof claims.

The separate finite [static IOMMU confinement model](docs/iommu-confinement.md)
adds generation-bound device assignments and domains, capability-derived IOVA
mappings, live backing-frame lifetimes, and read/write direction checks.
Lean proves model-level read confidentiality and write integrity for one step
and finite traces, plus non-forgery, attenuation, cleanup, lifetime, and
owner-isolation facts. The deny-all q35 snapshot remains unchanged. No VT-d
programming, IOTLB mechanics, assigned-device QEMU path, generated boundary,
or final-binary/hardware confinement claim is included.

The finite [deterministic VT-d boot plan](docs/vtd-boot-plan.md) projects that
static device-domain model into the bounded root/context remapping tables a
future boot slice will install for the pinned `intel-iommu` unit, which the
shared q35 builder now constructs on every mandatory emulator run with every
remapping-relevant option pinned and drift-rejected. Lean proves a
canonical two-word entry codec (round-trip, image, and injectivity), that every
accepted plan is the deny-all projection of an accepted `IOMMU.State` mapping no
frame, that the remapping-table frames are reserved and disjoint from the CPU
page tables, and a fixed fail-closed activation order. A host-only generator
emits the checked tables. The boot image maps the unit's MMIO window as the
one reviewed non-identity page-plan leaf (supervisor-only, no-execute, with
live-mutation fixtures), validates the quiescent unit against the pinned
registers, then installs the generated deny-all tables from scrubbed reserved
frames and enables translation in a fixed fail-closed order — publish root,
invalidate context cache and IOTLB, enable, verify enabled status and empty
fault state — with each step journaled and the final state accepted by the
generated `leanos_validate_vtd_activation` boundary before CPL3. Every
outbound CPL3 gate re-observes the enabled state and live tables, and source
and final-ELF policy checks confine every MMIO write site and pin the
activation order. Bus masters stay disabled, so the enabled deny-all tables
translate no DMA; the assigned-device path and any hardware refinement claim
remain out of scope.

The bounded [direct-port-I/O authority model](docs/direct-port-io.md) separates
untrusted port/value words from kernel-selected purpose, models the selected
IOPL-zero and deny-all TSS I/O-map controls, and proves that user-origin
requests preserve the identical complete device projection. Typed kernel
acceptance is confined to exact serial, PIC, PIT, and debug-exit manifest keys
including direction and width. TSS loading, x86 privilege and exception
semantics, device behavior, generated code, and the final binary remain outside
these model-level claims. The composed
[port-denial containment slice](docs/direct-port-io.md) sequences that user
denial with the atomic user-fault cleanup/survivor dispatch and proves that a
denied port attempt leaves the device projection unchanged and retires the
faulting subject without letting untrusted port/value/width words select a
kernel operation or survivor, or return to the faulting subject.

The finite [fast privilege-entry control model](docs/privilege-entry-control.md)
admits only the manifest-backed `int 0x80` system-call mechanism, requires a
kernel-produced and read-back EFER/fast-entry-MSR denial tuple, composes the
extended-state control snapshot, and confines normalized raw alternate-entry
denials to the authoritative current subject. CPUID/MSR access, instruction and
exception semantics, assembly, QEMU, and the final binary remain trusted or
tested boundaries rather than theorem claims.

The physical-frame allocator reference model and its representation,
complexity, initialization assumptions, proved invariants, and capability
ownership boundary are documented in
[`docs/frame-allocator.md`](docs/frame-allocator.md).

The bounded [Multiboot2 memory-map model](docs/boot-memory-map.md) validates a
typed handoff, conservatively normalizes page intervals, proves usable-frame
soundness, and refines its output into the physical-frame allocator.

The [firmware handoff corpus](docs/firmware-handoff-corpus.md) replays
captured real-firmware E820 maps and MADTs (Hyper-V UEFI, SeaBIOS, and OVMF
today) through the same Multiboot2 and topology decoders, converted
deterministically with provenance and pinned expectations, and holds both the
Lean definitions and the generated C to every result word, including fourteen
derived mutations per capture.

The [boot-reservation overlay](docs/boot-reservations.md) checks a finite
boot-artifact manifest and gives its frames unconditional precedence before
allocator initialization.

The [boot-time allocation slice](docs/boot-allocation.md) preserves and checks
the Multiboot2 handoff, reserves live boot artifacts, scrubs one bounded
identity-mapped frame, and publishes it only after the exact QEMU trace records
completion.

The first composition of capability authority with frame ownership uses
never-reused object identifiers to prove safe release and reuse; its lifetime
rule, machine-checked guarantees, executable attacks, and limits are documented
in [`docs/memory-lifecycle.md`](docs/memory-lifecycle.md).

Fixed boot-admitted [per-subject frame budgets](docs/frame-budgets.md) partition
eligible allocator frames, charge allocation to trusted kernel context, preserve
credit exactly across release and termination, and prove that a peer with an
available commitment can allocate independently of another subject's exhaustion.
Capability delegation does not transfer or duplicate the original charge.

The executable virtual-mapping model adds subject-owned address spaces,
capability-bounded read/write mappings, live translation checks, and stale
mapping invalidation. Its policy, proved scope, examples, and limitations are
documented in [`docs/virtual-mapping.md`](docs/virtual-mapping.md).

The executable [x86-64 page-table refinement model](docs/x86-page-tables.md)
encodes that policy into a constrained 4 KiB, four-level paging subset and
proves structural validity, permission non-amplification, current-frame
agreement, NX enforcement, and cross-address-space separation. Hardware walks,
CR3/TLB operations, boot integration, and the compiler remain trusted.

The finite [single-core TLB model](docs/tlb-model.md) makes invalidation atomic
with mapping/lifecycle mutation and revalidates cached translations against the
current encoded walk and allocator ownership before use. The boot image also
executes the canonical generated address-space-2/page-7 unmap effect against a
bounded runtime-mutable window, with ordered PTE-store/`invlpg` and
PTE-store/CR3-reload paths, a checked four-phase mutable-leaf relation that
keeps every other leaf exact, and kernel-observed before/replacement-frame
values. At the authoritative model boundary, current-root unmap preparation
derives subject and address space from the execution latch, retains both public
mapping projections, and publishes the acknowledged successor into the shared
virtual-memory/TLB state while preserving the folded runtime invariant.

The first total syscall model separates trusted caller/active-address-space
context from untrusted fixed-width scalar words and proves invariant
preservation, rejection stability, and caller confinement. Its vocabulary and
trust boundary are documented in [`docs/syscall-model.md`](docs/syscall-model.md).

The endpoint IPC model provides capability-authorized, capacity-one,
nonblocking mailboxes with trusted sender provenance, never-reused endpoint
identities, and complete destruction cleanup. Its precise proof boundary and
exclusions are documented in [`docs/endpoint-ipc.md`](docs/endpoint-ipc.md).

The [blocking-IPC boot slice](docs/adr/0009-blocking-ipc-boot.md) exercises a
causal B-block, A-send/wake, trusted redispatch, and exact delivery across the
Lean adapter, hosted oracle, generated freestanding code, and QEMU.

The bounded [capability-transfer model](docs/capability-transfer.md) attaches
at most one sealed, attenuated descendant to an endpoint envelope and installs
it atomically on receipt without interpreting payload words as authority.

The bounded [user-copy model](docs/user-copy.md) prevalidates a small complete
range through current virtual mappings before changing typed kernel buffers or
live-frame byte memory, with explicit alias rejection and atomic failure.

The [frame-scrubbing model](docs/frame-scrubbing.md) atomically clears reused
frame contents before publishing a fresh memory-object lifetime and proves
modeled reads cannot expose an earlier owner's bytes before the new owner
writes.

The [subject-lifecycle model](docs/subject-lifecycle.md) gives subjects
never-reused identities and defines atomic termination cleanup across held
capabilities, exclusively owned memory, address spaces, endpoints, pending
provenance, and runnable/current state. Its creation operation publishes a
fresh identity; it does not inherit or duplicate another subject's state.

The [bounded lifetime-identity issuers](docs/lifetime-identity.md) make
kernel-owned, finite counters the authoritative creation path for subject and
object lifetimes: every accepted creation returns the unique next
representable 64-bit identity, one object authority spans the memory,
endpoint, and address-space kinds, rejected or exhausted creation preserves
the complete runtime, and retired identities can never be made live again.

The bounded [model-oracle corpus](docs/model-oracle.md) is evaluated in Lean
and replayed through hosted generated code and every boot-reachable adapter.
This differential check detects integration mismatches; it is not compiler or
binary verification.

The [interrupt model](docs/interrupt-model.md) gives the initial page-fault,
timer, and syscall vector vocabulary, proves origin-sensitive dispatch and
whole-subject user-fault containment, and records the unproved x86 entry and
return boundary.

The atomic [user-fault dispatch model](docs/fault-dispatch.md) composes the
normalized CPL3 page-fault record with the authoritative lifecycle, scheduler,
resumable-context, mapping, and TLB state. It terminates exactly the kernel-owned
current subject and returns either the deterministic survivor context or typed
idle without exposing partial cleanup. Terminal outcomes retain the exact
typed inbound rejection cause, with separate kernel-origin and already-halted
classes, while changing only the halt latch.

The bounded inbound entry manifest and total trap-frame normalizer bind those
ordinary gates to explicit x86 raw shapes and kernel-owned subject, address
space, CR3, stack, purpose, and nested-entry state before a boot handler runs.
The layered [canonical page-fault snapshot](docs/page-fault-snapshot.md)
then derives read/write/execute and protection class from the exact supported
error bits, binds CR2 to its 4 KiB page, confines diagnostics, and publishes a
versioned fixed-width codec without claiming x86 or binary refinement.

A separate terminal vector-2 manifest models NMI snapshots on dedicated IST2
and proves that an exact CPL3 or CPL0 event, including one observed during an
ordinary handling step, freezes every modeled subsystem and enters the same
absorbing halt latch without return, scheduling, or CR3 continuation. The boot
image installs the matching DPL0 vector-2 gate and dedicated IST2 stack; a
mandatory QEMU monitor-injection probe observes real delivery across IF=0 and
the terminal assembly record after the kernel reports `NMI-READY`.
Delivery/blocking, frame construction, and the compiler/emulator path remain
trusted tested boundaries rather than theorem claims.

The [boot-interrupt phase model](docs/interrupt-model.md) replaces the
inherited bootloader IDT in the entry prologue. A finite Lean contract fixes
the `inherited → bootstrap32 → bootstrap64 → runtime → terminal` publication
chain with per-phase tables, descriptor widths, stack assumptions, and
terminal targets, and proves that every admitted bootstrap event latches an
absorbing terminal record without touching business state, return authority,
or the publication order. The image publishes a statically decoded 32-bit
bootstrap IDT before any other boot work, hands off to the 64-bit bootstrap
table in the instruction after long-mode activation, and keeps every early
vector — including NMI — on reviewed non-returning terminal stubs until
`privilege_init` publishes the runtime manifest over valid TSS/IST state. The
trusted window narrows to the reviewed eleven-instruction pre-`lidt` prologue
and that single-instruction handoff boundary; final-ELF policy decodes both
bootstrap tables gate-by-gate, bounds each stub's terminal CFG, and
inventories every `lidt`/`sidt`. Two mandatory QEMU probes exercise both
sides of the handoff — a real pre-paging `ud2` latched by the bootstrap32
catch-all with an exact `vector=6 reason=invalid-opcode` terminal record, and
a monitor-injected NMI latched by the bootstrap64 vector-2 stub after an
exact early-only readiness checkpoint, before the runtime IDT exists. Real
descriptor semantics, delivery inside the residual window, and the final
binary remain trusted/tested boundaries.

The [fail-stop model](docs/fail-stop.md) adds an irreversible execution latch,
bounded double-fault escalation, and one absorbing gate for every modeled
post-fatal mutation and context-restoration path.

The [double-fault IST slice](docs/adr/0007-double-fault-ist.md) installs a
dedicated guarded stack for vector 8 and exercises one deterministic QEMU
fail-stop path. This is machine-integration evidence, not proof of x86
exception delivery or of the resulting binary.

The [observer-relative isolation model](docs/observation-model.md) defines a
subject's authorized view and proves scoped one-step low-equivalence and equal
visible replies for unrelated sequential operations over disjoint actor-local
memory. Authorized IPC and aliased shared memory/capabilities, global resource
exhaustion, and visible scheduling are explicit
channels; this is not a binary-level or timing-sensitive confidentiality claim.

The [finite scheduled observer-isolation model](docs/scheduled-observation.md)
composes that view with the bounded scheduler and proves a
termination-insensitive paired finite-prefix theorem with explicit public
channels and silent-step stuttering. It remains a Lean model result, not a
refinement claim for the boot slices or machine code.

The [security claim index](docs/security-claims.md) collects the stable,
machine-checked propositions that form the currently advertised proof surface,
including their assumptions, evidence classes, and explicit exclusions.

## Verification targets

These are long-term directions, not claims that the completed slices satisfy an
entire verification target. Work lands incrementally with an explicit threat
model and proof statement.

- **Functional correctness:** kernel operations refine a small abstract state
  machine and satisfy documented API contracts.
- **Capability safety:** authority is explicit, unforgeable in the model, and
  cannot be amplified by kernel operations.
- **Isolation and information flow:** subjects cannot observe or modify state
  outside their authority, modulo documented channels and assumptions.
- **Memory safety:** allocation, mapping, and object lifetimes preserve
  separation and ownership invariants.
- **Crash and recovery behavior:** persistent operations have specified atomic
  outcomes under modeled interruption.
- **Liveness and resource bounds:** selected operations terminate and critical
  resources have enforceable limits.
- **Boot integrity:** measured artifacts correspond to reviewed sources and a
  documented build process.

## CI strategy

GitHub-hosted Linux runners can run QEMU without hardware acceleration. That is
slower than KVM but suitable for a small, deterministic boot-smoke test.

CI will grow in layers:

| Layer | Gate | Status |
| --- | --- | --- |
| Repository | Markdown and repository hygiene | Active |
| Lean | Build all modules and check proofs with a pinned toolchain | Active |
| Host tests | Generated-C oracle and boundary/harness regressions | Active |
| Emulator | Build and boot headlessly with timeout and serial assertions | Active |
| KVM evidence | Replay the PR-tier matrix with explicit hosted KVM | Experimental, non-blocking |
| Artifacts | Preserve image, ELF, map, checksums, versions, and serial log | Active |
| Release | Publish tagged reproducible images with provenance | Active |

Emulator CI should invoke one repository-owned script, use an explicit timeout,
capture the serial console, and require a guest success signal. A process that
merely stays alive or prints part of a boot log is not a passing test.

There is no deployment target yet, so continuous deployment would be premature.
Once a bootable artifact exists, tagged releases can publish images and build
provenance; real-hardware deployment should remain a separate, opt-in test lane.

### Lean development

Install [Elan](https://github.com/leanprover/elan), then run the repository-owned
check from the repository root:

```sh
./scripts/check.sh
```

Elan reads `lean-toolchain` and installs the exact Lean release automatically.
The check builds every default Lake target and verifies that the deliberately
invalid proof fixtures remain rejected. Lean warnings are errors for project
modules, so declarations containing `sorry` or `admit` fail the build. The
check also rejects unapproved `axiom`, `constant`, `unsafe`, and `extern`
declarations; required trusted-code boundaries must be documented and explicitly
allowlisted when they are introduced. It separately reports every semantic
`native_decide` use by source module, requires a reviewed policy classification,
and rejects direct source use of `Lean.ofReduceBool`; these proofs are
machine-checked under the documented native-evaluation TCB, not kernel reduction
alone. GitHub Actions invokes the same script; generated Lake output is kept
under the ignored `.lake/` directory.

### Local CI commands

The pull-request workflow uses only these repository-owned entry points:

```sh
./scripts/check-markdown.sh
./scripts/check.sh
LEANOS_BUILD_TIMING_FILE=build/ci/image-build-phases.tsv \
  ./scripts/build-image.sh
./scripts/record-tool-versions.sh
./scripts/run-emulator-evidence.py run
./scripts/run-emulator-evidence.py bundle
```

The first command requires Node.js/npm. `check.sh` also runs the controlled
image-build compiler-failure fixture, so it requires the image-building tools
listed below even though that fixture intentionally stops before packaging.
CI runs this fixture once in the required Lean lane, not in each QEMU shard.
The final command writes one tarball
whose internal manifest hashes the retained evidence and rejects missing
report-bound files. Image building and QEMU prerequisites,
the exact Ubuntu 24.04 package versions used in CI, and emulator resource bounds
are listed in [the boot-image guide](docs/boot-image.md). The versioned
toolchain profiles described in
[ADR 0014](docs/adr/0014-toolchain-compatibility-profiles.md) keep the canonical
byte-reproducible GCC release profile distinct from the exact Clang profile's
semantic-compatibility evidence. A separate daily and path-triggered
[compatibility workflow](docs/toolchain-compatibility.md) compares bounded,
same-revision semantic evidence across all registered profiles and records the
observation history needed for candidate promotion. CI first runs the
Markdown and complete Lean proof-integrity gates, then builds once and executes
the versioned mandatory emulator matrix without KVM. The matrix is the sole
release-blocking QEMU inventory for pull requests and tags. A separate
non-blocking lane replays the four PR-tier shards only after an explicit
no-fallback KVM probe succeeds; its evidence and promotion policy are defined in
[ADR 0013](docs/adr/0013-kvm-on-host-evidence.md). CI retains images,
debug ELFs, symbol maps, checksums, pinned tool versions, serial logs, exact
commands, and the machine-readable evidence report in one manifest-bound
tarball per emulator shard for 14 days, including available diagnostics from
failed runs. Image-producing lanes also retain the validated six-phase timing
records described in [the boot-image guide](docs/boot-image.md), so issue #266
performance work can compare measured phases without treating timing as a
reproducibility input. Controlled negative fixtures ensure
theorem, compiler, matrix-inventory, artifact-hash, serial-protocol,
guest-signal, and timeout failures cannot pass.

Tags matching `vMAJOR.MINOR.PATCH` additionally run that same matrix, require a
byte-identical double build, and publish its evidence manifest with checksums
and GitHub provenance. The version policy,
artifact inventory, trusted-boundary warning, and download verification
commands are in [the boot-image guide](docs/boot-image.md).

## Roadmap

### Phase 0: foundations

- define the scope, threat model, target platform, and proof vocabulary;
- pin Lean, Lake, QEMU, linker, and cross-compilation dependencies;
- test the freestanding Lean/runtime boundary and record the architecture
  decision; and
- establish local commands that CI invokes without duplicating build logic.

### Phase 1: proved boot slice

- create a minimal bootable image and serial-console protocol;
- define the first abstract kernel state and operation;
- prove its key invariants and connect it to the boot demo; and
- run proof, build, and QEMU smoke checks on every pull request.

### Phase 2: capability microkernel core

- introduce kernel objects, capabilities, and address spaces;
- specify and prove authority-preservation properties;
- add memory allocation, mapping, IPC, and syscall boundaries one slice at a
  time; and
- expand adversarial model tests and emulator scenarios.

### Phase 3: system services

- move policy into isolated user-space services;
- explore verified storage, networking, and recovery components; and
- add hardware-backed test lanes without weakening deterministic QEMU CI.

Process duplication is deliberately excluded from this roadmap. LeanOS does
not promise `fork()`, a fork syscall, or a clone-like operation with implicit
inheritance. [ADR 0010](docs/adr/0010-defer-fork.md) defines the whole-kernel
readiness gate. Any future implementation must begin with a new architecture
issue that closes every item in that gate before defining a model, ABI,
adapter, or boot path.

## Contributing

The initial backlog is maintained in
[GitHub Issues](https://github.com/rudi-cilibrasi/leanos/issues). Before opening
a pull request:

1. link the issue or design question the change addresses;
2. distinguish proved properties from tested behavior;
3. document any new TCB assumption or unverified boundary;
4. run the same repository scripts used by CI; and
5. keep the change to one reviewable vertical slice.

Architecture-changing work should begin with a short issue or decision record.
Proofs are part of the implementation: changes that invalidate them should fix
or deliberately revise the associated specification in the same pull request.

## Reading the evidence

Use the [security claim index](docs/security-claims.md) for the current proved
surface, the accepted [architecture decisions](docs/adr/) for scenario-specific
claims and TCB additions, and the [boot-image guide](docs/boot-image.md) for
reproduction commands and exact QEMU evidence. LeanOS should continue to be
described as an experimental research project rather than a verified operating
system.

leanos

Owner Repos

File Explorer

# Use via CDN

# Project Badges

Was this content helpful?

Recent Feedback

leanos

Owner Repos

File Explorer

# Use via CDN

# Project Badges

Was this content helpful?

Recent Feedback

Download README