Concept

Network invariants

An invariant is a rule that must hold for a network state to be acceptable — for example, "no link refers to a missing interface" or "segment A must always reach segment B". In RAHN, the set of invariants in force is called the constitution, and it is data, not code reviews.

The structural floor

Every RAHN state automatically carries a floor of structural invariants (invariants specification):

The constitution layer

On top of the floor, a constitution file declares named constraints evaluated over the node graph induced by interface links: require-connectivity a b and prohibit-connectivity a b (constitution specification). The vocabulary is deliberately small and decidable; what it can and cannot express against real-world invariants is research question RQ4, which is open.

Deterministic evaluation

Invariant evaluation is deterministic: same state, same constitution, same verdict — on every machine, every run. Failures are explainable by design: an error carries the violated invariant, the offending objects, and the transition that produced them. Violations are data, which is what makes CI integration with an exit-code contract possible.

The epistemic honesty rule

The constitution only protects what it encodes. "Verified" means "all encoded invariants hold" — nothing more. This is stated as a limitation, not a footnote: limitations, item "verification is only as good as its encoding". Expressiveness work (what real incident-derived invariants the vocabulary can capture) is a contribution path, not a closed question.

Where to go next