Shape transition, reachability, and fail-closed reasoning

ZenoDEX Shape Pruning Lab

This lab treats the old ZenoDEX shape and the achieved audited-domain Shape++ release as clause sets. Toggle the clauses, select a scenario, and inspect which disaster states remain reachable, which are pruned, and which boundary faults fail closed under the active shape.

Q (full state space) D Reach(M)

Clause board

The baseline clauses already block several bad worlds. The strengthening clauses push more invalid, ambiguous, or drift-prone worlds out of reach.

State-space board

The selected scenario branches at one pipeline stage. Under a stronger shape it is redirected into reject or recover, not disaster.

blocked, the active shape removes this bad branch
fragile, some guards exist but the proof boundary is still incomplete
reachable, the bad state is still admissible under the active shape

Reasoning trace

Scenario facts

Scenarios and chaos probes

Some scenarios are already blocked by the baseline. Others only disappear once the new clauses become active and the runtime fails closed on mismatch.

Chaos probes

Reading rule: a green probe does not mean "proved forever." It means the currently active shape has the clauses needed for the intended fail-closed posture under that perturbation.