v0.48.0 - Formal PeerRiskSignal Verification (Tamarin)
Formal PeerRiskSignal Verification (Tamarin)
Closes the Third Trust Cycle (v0.38–v0.48) with formal proofs over the PeerRiskSignal state machine.
What is new
Three Tamarin Prover security lemmas in ops/tamarin/risk_signal/peer_risk_signal.spthy:
| Lemma | Status | Proves |
|---|---|---|
signal_bounded |
Proved | Signal value always in {low, mid, high} (abstracting [0.0, 1.0]) |
anomaly_detection_responsive |
Proved | SuddenDrop cannot permanently suppress anomaly detection |
no_single_source_cascade |
Proved | Cascade amplification requires genuine independent observations from each detecting sovereign |
Executable property tests (no Tamarin required)
genesis_mesh/tests/test_risk_signal_formal.py — 13 property-based tests covering signal boundedness, anomaly responsiveness, and cascade isolation.
genesis_mesh/tests/test_risk_signal_tamarin.py — pytest wrappers that invoke tamarin-prover --prove; skip automatically when tamarin-prover is not installed.
What is NOT proved
- Implementation fidelity (Python bugs, floating-point precision)
- Timing attacks on the continuous decay formula
- Cross-sovereign collusion (two observers coordinating)
Tests
17 new tests (14 pass unconditionally; 3 Tamarin runners skip without tamarin-prover).
Full suite: 1041 passed, 4 skipped.
Third Trust Cycle complete
v0.38–v0.48: adversarial hardening, communication privacy, overlay discovery, process-level mediation, trust path performance, data usage attestation, formal verification.