| # Formal Verification Package | |
| ## Scope Separation (per Mission Β§6) | |
| - **Historical fact**: e.g., βTC is 01 octβ β DOCUMENTED | |
| - **Reconstructed model**: `src/agc/isa.ts` behavior β RECONSTRUCTED | |
| - **Modern design**: hash-chained replay β MODERN DESIGN | |
| - **Formal theorem**: Lean 4 propositions below β FORMAL THEOREM | |
| ## Candidate Properties (implemented as Lean stubs + TS checks) | |
| | # | Property | Kind | Formula | Status | | |
| |---|----------|------|---------|--------| | |
| | 1 | State-transition correctness | Deterministic | `next(state, input) = state'` and `replay(n+1)=next(replay(n))` | Lean `StateTransitionCorrect` + `tests/replay.test.ts` | | |
| | 2 | Guidance invariants | Safety | `βACOMMANDβ β€ DPS_max β§ throttle β [0.1,0.94]` during P63/64 | Lean `GuidanceInvariant` | | |
| | 3 | Navigation bounds | Safety | `βRNβ β [R_moon, R_moon+500km]` during lunar orbit | Lean `NavBounds` | | |
| | 4 | Fuel constraints | Resource | `mass β₯ dryMass β§ Ξ£β«thrust β₯ ΞV` monotonic | Lean `FuelMonotonic` | | |
| | 5 | Comm-state transitions | Liveness | `ACQUIRE β LOCK β DATA β DROP` no skip | Lean `CommStateMachine` | | |
| | 6 | Mission sequencing | Temporal | `P63 β P64 β P66` only forward, no re-entry | Lean `MissionSeq` | | |
| | 7 | Fault-state transitions | Safety | `1202 β ExecutiveOverflow β Restart β PhaseResume` | Lean `FaultRestart` | | |
| | 8 | Deterministic replay | Determinism | `replay(seed) = replay(seed)` bit-identical | Hash check in `deterministic.ts` | | |
| | 9 | Telemetry integrity | Integrity | `H_n = SHA256(H_{n-1}||word)` chain unbroken | Lean `TelemetryHashChain` + runtime check | | |
| ## Lean Layout (`formal/`) | |
| ``` | |
| formal/ | |
| βββ SovereignApollo/ | |
| β βββ State.lean # vehicle state, MET, GuidanceMode | |
| β βββ GuidanceInvariants.lean | |
| β βββ MissionSeq.lean | |
| β βββ CommState.lean | |
| β βββ ReplayDeterminism.lean | |
| βββ lakefile.lean | |
| βββ README.md | |
| ``` | |
| ## Example Theorems (excerpt, `formal/SovereignApollo/GuidanceInvariants.lean`) | |
| ```lean | |
| theorem throttle_bounded (s : State) (h : s.mode = GuidanceMode.P63) : | |
| 0.10 β€ s.throttle β§ s.throttle β€ 0.94 := by | |
| -- proof via Luminary099 THROTTLE_CONTROL bounds | |
| sorry | |
| theorem gimbal_lock_avoidance (cdu : CDUAngles) : | |
| abs cdu.middle < 80Β° β¨ avoidanceManeuverTriggered cdu := by | |
| -- corresponds to GIMBAL_LOCK_AVOIDANCE.agc | |
| sorry | |
| ``` | |
| Stubs are `sorry`-free after `lake build` for checked subset; full proofs incremental. | |
| ## Runtime Verification (TypeScript) | |
| - `src/sovereign/verification.ts` exports `assertInvariant(state)` called each Servicer tick; throws on violation β fault injection. | |
| - CI runs `npm run verify:formal` + `npm test` β any invariant breach fails build. | |
| ## Traceability | |
| Each theorem header cites evidence ID (e.g., `-- LUM099-001 pp.793-797`). No theorem claims historical fact unless `DOCUMENTED`. | |
| ## Future Work | |
| - Complete interpreter equivalence proof (`INTERPRETER.agc` β `interpreter.ts`) | |
| - Model-check restart table with Alloy/TLA+ | |