# Formal Verification (Z3): Detector Logic

**System:** MetaSpace.bio FDIR detector guard
**Status:** machine-checked proof of *implementation conformance to the specification*. Reproduce with `python verify_guard_conformance.py`.

---

## 1. What is proved

The detector function `backend/modules/fdir_guard.py` (used by the simulator for GPS and IMU fault decisions) is proved, with the Z3 SMT solver over IEEE-754 float64 arithmetic, to conform to the formal specification `satellite_fdir.bio` **for every possible input**, including infinities and NaN:

| ID | Property |
|----|----------|
| S1-S5 | For each of the five channels: residual magnitude at or above the `.bio` threshold implies `fault_detected` |
| S6 | All channels below their thresholds implies no fault (no false alarm) |
| S7 | `fault_detected` implies `safe_mode` |
| S8 | Any NaN input implies `fault_detected` (fail-safe on invalid sensor data) |
| S9 | `fault_code` is in 0..5 and is non-zero exactly when a fault is detected |
| S10-S14 | If only channel *i* is breached, the fault code identifies channel *i* |
| S15 | A nominal input vector is accepted (the specification is not over-constrained) |

The thresholds are parsed from the `.bio` file, and the guard carries independent constants, so any drift between the two is caught as a counterexample.

## 2. How the proof is made trustworthy

- **The proof is about the source file.** The Python source of the guard is parsed (AST) and symbolically executed into a Z3 floating-point term; it is not a hand-written model.
- **Differential test:** the translated term is evaluated on 1565 boundary, NaN, infinity and random vectors and compared with the real Python function: 0 mismatches.
- **Mutation controls:** eight deliberately broken guards (changed boundary, wrong threshold, missing absolute value, NaN-unsafe comparison, safe mode never set, channel dropped, swapped fault codes) are each rejected with a counterexample.

## 3. What is NOT proved

- That the thresholds are physically correct. Wheel (0.05 N·m) and battery (0.5 V) thresholds are illustrative.
- That the simulator's `gps_error` is a distance in metres (it is a dimensionless score treated here as the guard's residual).
- That the specification is more than a set of threshold comparisons. Both the specification and the guard are "residual against threshold" rules, so the proof protects against implementation slips (boundary, sign, `abs()`, NaN handling, fault-code wiring, safe-mode wiring); it does not show that a physical fault is detected.
- Anything about the power fault logic (battery level, solar output), which is outside the guard.
- Real-time latency, failure rates (PFD) or behaviour on flight hardware.
- The correctness of Z3, of CPython's float semantics, or of the AST translator itself (the translator is validated by the differential test and the mutation controls, not proved).

## 4. Earlier finding fixed by this work

The earlier `>` comparisons in the simulator did not trigger on a NaN sensor value and differed from the specification's `>=` at the exact threshold. The guard fixes both, and the proof covers them.