no divergence detected
Structural diff is silent on this constraint pair.
SpecGap · assurance report replay
We preserve disagreement instead of collapsing it into false confidence.
Three independent verdicts on one specification stack.
counterexample found
Policy permits behavior the intent forbids in the abstract model.
disagreement preserved
Both signals kept — not merged into one verdict.
Case Read-only root vs /var write permission
report 8f2a1c9d4e7b3065… · seed 42
Replay cases
Worked case
Step through the report
Stakeholder intent
The root filesystem is read-only per container policy.
Formalized policy
Write access to /var is allowed for application logs and runtime state.
Implementation claim
Write access to /var is allowed for application logs and runtime state.
Counterexample
The gap, made concrete
Formalized Policy ⇒ Stakeholder Intent
Each layer reads fine in isolation. Together, the model permits behavior the intent forbids.
AssignmentMeaning
fs_write = true→a filesystem write occurs
write_other = true→a write occurs outside the allowed scope
Policy text looks locally reasonable. Z3 found a concrete behavior the stakeholder intent forbids. SpecGap reports both: structural silence and an implication failure.
Optional inspection
Collapsed by default. Expand to view fixture summary, CLI, or MCP invocation for this replay.
View report fixture (summary)
{
"id": "structural_miss",
"title": "Read-only root vs /var write permission",
"timestamp": "2026-05-19T14:32:07Z",
"version": "0.1.0",
"seed": 42,
"reportHash": "8f2a1c9d4e7b3065a1f0c8d2e9b4a7f1",
"verdicts": [
{
"kind": "structural",
"status": "pass",
"headline": "no divergence detected"
},
{
"kind": "z3",
"status": "fail",
"headline": "counterexample found"
},
{
"kind": "triangulation",
"status": "warn",
"headline": "disagreement preserved"
}
],
"counterexample": [
{
"variable": "fs_write",
"value": "true",
"interpretation": "a filesystem write occurs"
},
{
"variable": "write_other",
"value": "true",
"interpretation": "a write occurs outside the allowed scope"
}
]
}View CLI invocation
cd specgap python -m specgap.cli examples/06_triangulation_disagreement.json --out reports/triangulation.md
Source: examples/06_triangulation_disagreement.json
View MCP request
tool: analyze_spec
input: {"path":"examples/06_triangulation_disagreement.json","extractor":"rule"}View report hash + metadata
scenario_id: structural_miss report_hash: 8f2a1c9d4e7b3065a1f0c8d2e9b4a7f1 timestamp: 2026-05-19T14:32:07Z seed: 42 version: 0.1.0 fixture: demo-site/data/fixtures/structural_miss.json
Bounded assurance
What SpecGap is — and is not
In scope
- Extract constraints from layered spec text
- Compare layers structurally
- Check implication with Z3 (abstract model)
- Preserve disagreement between mechanisms
Out of scope
- Runtime verification
- Proof that a sandbox is safe to run
- Deployment or infrastructure correctness
- Replacing BoxArena or enforcement layers
- Free-form natural language understanding
Trust boundary
SpecGap stops at evidence — not runtime proof
BoxArena tests adversarial runtime behavior. It sits outside this boundary and does not re-check specification alignment.