Concept

Network verification

Verification is the act of proving that a network state satisfies its declared rules before the state changes or anything executes. In RAHN it is not a review step — it is a structural gate that cannot be bypassed.

The gate

Every commit must pass the constitution of invariants. If an invariant fails, the transition is rejected with an explanation that names the violated invariant, the offending objects, and the transition that produced them. The execution path is structurally unreachable without a verification result — not discouraged, unreachable. Real execution additionally requires explicit opt-in (--execute --yes-i-know) and runs only in isolated Linux network namespaces (see simulation-first execution).

Verification in CI

Since v0.8 (ADR 0017), rahn test [ref] produces a deterministic, machine-readable verification report over any committed state, with an exit-code contract (0 = verified, 1 = violation, 2 = usage error) so pipelines can gate on it. Invariant ids are a machine contract. An example GitHub Actions gate ships in examples/network-ci.yml.

What "verified" means — and does not

This is the honesty rule at the center of RAHN's epistemology: "verified" means "all encoded invariants hold" — nothing more. Verification is only as good as its encoding; unencoded failure modes pass. RAHN never presents a green check as a general safety claim, and the limitations baseline says so in those words.

Open research

Verification cost at scale is research question RQ2: the invariant engine is implemented for the v0.1 vocabulary, but the latency distribution across 10²–10⁵ objects has not yet been measured (experiment E2). Constitution expressiveness — which real-world invariants the language can encode — is RQ4. Both are open to contributors; see contributing.

Where to go next