One runtime path from uncertain upstream input to deterministic downstream execution control. Not a model. No weights. No probabilistic output. A hard boundary that authorizes, blocks, or stops -- and produces cryptographically verifiable evidence for every decision.
Models generate proposals. Sensors generate observations. Between them and real-world execution, the authorization boundary is often fragmented, implicit, or unverifiable.
The kernel sits at the last point before actuation. Contradiction reduces available actions to zero: BLOCK, plus a cryptographically verifiable receipt explaining why. MGOS preserves conflict -- never averages.
The kernel blocks execution when upstream sources conflict or policies fail. No exceptions. No averaging.
The Integrity Engine does not smooth contradictions. Disagreement between sources is retained as a diagnostic signal.
Same stabilized state under the same policy always produces the same result. Core authorization logic formally verified in Lean 4.
Every authorization produces a cryptographically verifiable receipt: SHA-256 hash, manifest, timestamp. Tamper-evident. Replayable.
Core authorization logic proved in Lean 4:
Implementation layer:
Black-box test suites:
Gate between planner output and actuator execution. STOP on constraint violation. Receipt for post-flight audit.
Enforce operational envelopes. Hash-verified state before valve, relay, or motor commands. Fail-safe on sensor disagreement.
Pre-trade compliance gate. Deterministic BLOCK on limit breach. Full receipt chain for regulatory audit.
CI/CD gate, deployment authorization, privileged actions. Evidence bundle for post-incident forensics.
One product -- MGOS Runtime Stack (MGOS Integrity & Authorization Runtime). Five layers, each with a clear role.
Evidence bundle delivered under NDA within 24h. Offline-verifiable. MANIFEST / SHA / VERIFY.