Aevion // The Gate Registry

13 formal gates.

Every gate is a Lean 4 theorem. Every theorem is proven. Every action produces a signed receipt.

nemoclaw.memory_store_path
MemoryStore.path_confined
[ Live ]
NIST: MANAGE
nemoclaw.conflict_of_interest
ConflictOfInterest.coi_gate_denies_undisclosed
[ Live ]
NIST: GOVERN
nemoclaw.session_expiry
SessionExpiry.session_not_expired
[ Planned ]
NIST: MANAGE
nemoclaw.capability_token
CapabilityToken.gate_authorized
[ Planned ]
NIST: GOVERN
nemoclaw.prompt_integrity
PromptIntegrity.prompt_not_injected
[ Planned ]
NIST: MEASURE
nemoclaw.output_grounding
OutputGrounding.output_is_grounded
[ Planned ]
NIST: MEASURE
nemoclaw.data_provenance
DataProvenance.training_data_write_authorized
[ Planned ]
NIST: MAP
nemoclaw.output_ip_clearance
IPClearance.output_ip_cleared
[ Planned ]
NIST: MEASURE
nemoclaw.action_reversibility
ActionReversibility.action_is_reversible
[ Planned ]
NIST: MANAGE
nemoclaw.delegation_chain
DelegationChain.delegation_chain_valid
[ Planned ]
NIST: GOVERN
nemoclaw.rate_limit
RateLimit.action_within_rate_bounds
[ Planned ]
NIST: MANAGE
nemoclaw.pii_scope
PIIScope.pii_not_exfiltrated
[ Planned ]
NIST: MAP
nemoclaw.human_oversight_required
HumanOversight.human_review_completed
[ Planned ]
NIST: GOVERN
Architecture

Compositional structure

Level 1: primitive gates — individual Lean 4 theorems. Level 2: compound gates — theorem composition (COI + path confinement). Level 3: multi-agent orchestration — Byzantine fault tolerance at the proof level.

Contribution

Adding a gate

Publish a Lean theorem and Python checker to config/formal_gate_registry.json. Aevion reviews: sorry-free, CI-passing, schema-compliant. Certification granted. The gate gets an aevion_verified badge.

Full registry →