# Archetype: config-infra (Config/DNS/Infrastructure)
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

**Applies to**: Configuration, DNS, infrastructure, IaC tools

## Common Proofs

### INFRA-1: Format validation

**Target**: `verification/proofs/idris2/FormatValid.idr`
**Prover**: Idris2
**Priority**: P0

**Statement**: All config files validated against schema before use.

**Obligations**:
- [ ] Define schema
- [ ] Prove loader requires valid config

---

### INFRA-2: Idempotent apply

**Target**: `verification/proofs/idris2/ApplyIdem.idr`
**Prover**: Idris2
**Priority**: P0

**Statement**: Applying same config twice is safe.

**Obligations**:
- [ ] Model apply op
- [ ] Prove idempotence

---

### INFRA-3: Rollback on failure

**Target**: `verification/proofs/tlaplus/Rollback.tla`
**Prover**: TLA+
**Priority**: P1

**Statement**: Failed apply rolls back to previous state.

**Obligations**:
- [ ] Model state + apply/rollback
- [ ] Model-check no stuck states

---

### INFRA-4: DNS record validity

**Target**: `verification/proofs/idris2/DNSValid.idr`
**Prover**: Idris2
**Priority**: P1

**Statement**: Generated DNS records conform to RFC 1035.

**Obligations**:
- [ ] Model DNS record types
- [ ] Prove format compliance

---

## Plus: Mandatory ABI proofs

ABI-1 through ABI-5.

## Repos using this archetype

cloudflare-dns-terraform, hesiod-dns-map, resource-record-fluctuator, rrecord-verity, twingate-helm-deploy, zerotier-k8s-link, ipv6-tools, ipfs-overlay, hybrid-automation-router, ambientops, kaldor-iiot, laminar, laniakea
