MGOS does not ask you to trust a story. It shows exactly which kernel properties are formally mechanized, which layers are engineered, and which operational claims are supported by auditable evidence.
In the current Lean artifact, the following model-level claims are proved:
MGOS does not prove arbitrary perception, sensor fusion, or upstream AI semantics. It proves the behavior of the small execution-boundary kernel once external evidence has already been mapped into the kernel decision domain.
This is deliberate. It keeps the trusted core small, auditable, and suitable for mechanization.
The current formal story is model-level first, with implementation-level transfer obligations stated explicitly rather than silently upgraded into theorem status.
These layers matter operationally. They are tracked in a different assurance layer than the Lean kernel.
Operational validation is not a theorem. It is a separate evidence layer designed to be replayable and externally auditable.
MGOS follows a zero-overclaim discipline. This is not a weakness in presentation. It is the proof architecture itself.
| Claim | Status | Scope |
|---|---|---|
| Fail-safe authorization rule | PROVED | Lean kernel model |
| Output exhaustiveness / totality | PROVED | Lean kernel model |
| Model-level determinism | PROVED | Pure functional model |
| Vote permutation invariance | PROVED | Lean permutation layer |
| TMR decision permutation invariance | PROVED | Lean permutation layer |
| Conflict safety | PROVED | Lean kernel model |
| Manual-override dominance | PROVED | Lean kernel model |
| Receipt composition (abstract) | PROVED | Abstract witness model |
| Bitwise determinism | CONDITIONAL | Pinned environment required |
| Target-level termination / WCET | CONDITIONAL | Platform evidence required |
| Stable concrete cryptographic receipts | CONDITIONAL | Concrete pipeline not fully mechanized |
| Normalizer verification | OPEN | N : E -> D remains primary transfer risk |
| Audited black-box suites | VALIDATED | Evidence packs / audited runs |
This is intended for independent review, not only internal demonstration.
Instead, it offers something narrower and more auditable: a deterministic execution-boundary kernel, a named proof boundary, and an evidence trail that can be inspected by third parties.