Agents that share state usually rely on eventual consistency and hope. Bide’s shared state rests on a convergence theorem that is machine-checked axiom-free, re-checked on three proof-assistant toolchains, and wired into the engine as a fail-closed gate, so a bug in the Go verifier cannot hand you a machine whose tables do not converge. This is what is proven, how it is checked, and exactly where the proof stops.
You rarely know everything before you have to start building. This is the workflow I use to build the parts that are settled, hold the parts that are not as defaulted decisions with known reversal costs, and never paint into a corner. Two anchors carry it: invariants made unrepresentable, and a decision register threaded through the code as a greppable ID.
You find an over-restriction because something legitimate breaks and points at the spot, and it breaks earlier the earlier you encode the rule. You do not find an over-permission the same way, because nothing legitimate ever exercises it. Here is the asymmetry, a worked example, and where it stops being true.