SpecGap
We preserve disagreement instead of collapsing it into false confidence.
Specification stack
Stakeholder intent
The root filesystem is read-only.
Formalized policy
Write access to /var is allowed for runtime state.
Implementation claim
Write access to /var is allowed for runtime state.
Structural
✓no divergence detected
Structural diff is silent on this constraint pair.
Z3 Implication
✗counterexample found
Z3 Implication
✗counterexample found
fs_write = true
write_other = true
Policy permits behavior the intent forbids in the abstract model.
Triangulation
⚠disagreement preserved
Both signals are kept — not merged into one verdict.
SpecGap stops at evidence — not runtime proof.
Inside TCB
- rule extractor
- weakening lattice
- abstract sandbox model
- Z3 checker
Outside
- runtime infrastructure
- deployment
- BoxArena
- production systems
Reproducibility
- 41/41 pytest
- 4 deterministic fixtures
- static replay
- report hash 8f2a1c9d4e7b3065a1f0c8d2e9b4a7f1
- no telemetry
- no live execution
Evidence, not certainty.