Architecture Philosophy: Rule-First Design

The Core Question

When building an engine to verify AI-written code, architects hit a brutal dilemma. Where do rules live, and who enforces them?

Axiom's answer is simple. Rules must precede code.

---

Rule-First Principle

Traditional software development works like this:

1. Write code first.
2. Run tests to catch bugs.
3. Add rules to prevent similar bugs.
4. Repeat forever.

This reactive approach shatters catastrophically when verifying AI-generated code. LLMs excel at crafting outputs that pass tests while concealing logical flaws—they're geniuses at creating "plausible wrong answers." Their probabilistic nature means bugs reappear in subtly different forms, bypassing test-based detection.

Without rules locked in first, the engine eventually gaslights itself. It starts lowering verification standards to accommodate AI hallucinations. A verification engine that discovers rules from code inspection ends up in a self-justifying loop. It validates code against constraints derived from that same code.

So Axiom inverts the paradigm completely:

1. Declare rules: Define invariants, contracts, safety properties first.
2. Encode: Transform rules into verification artifacts.
3. Prove: Mathematically prove code satisfies rules.
4. Execute: Only then allow execution.

---

Constitution-Ordinance-Annals: Layering Rules

Axiom splits rules into three layers. Structure borrowed from legal systems.

Layer	Keyword	File Pattern	Purpose	Change Frequency
Constitution	Context	CONTEXT.md	Immutable design principles	Almost never
Ordinances	Spec	docs/spec/*.md	Detailed algorithms and constraints	Moderate
Annals	History	docs/history/*.md	Decision records and history	Frequent

Layer 1: Constitution (Context)

Project identity. Principles like "Core calculations must use pure functions (func) only" belong here. Stuff that breaks the project's foundation. Modifying CONTEXT.md requires serious architectural review.

## 2. Core Architecture Principles (SSOT)

### Purity Hierarchy

- **Core Calculation Tier**: `src/core` computation uses `func` exclusively
- **Boundary Executor Tier**: `proc` exists only at OS/interfaces
- **Executor-only Rule**: Boundary `proc` cannot own business logic

Layer 2: Ordinances (Spec)

Actual running rules. SMT solver interfaces, Lean 4 proof strategies—concrete specifications live here. Guidelines during implementation.

• bmc_core.md: Model checking algorithms, Z3 interfaces, timeout rules
• uap_logic.md: Universal pipeline stages, counterexample promotion, invariant refinement
• lean_proof.md: Lean 4 semantics, tactic strategies, replay protocols

Layer 3: Annals (History)

Answers "why did we decide that back then?" Records past compromises and decision context. Annals are for reference only—they should never govern current implementation.

## 2026-03-26
- Core introduced Bottom-up Sorter, Vault Manager, Axiom Orchestration Loop
- Established stale axiom blocking and vault-based promotion paths

Annals stay separate from rules. When you need "why does this rule exist?" you check annals. When implementing code, you focus on constitution and ordinances. No wading through historical noise.

---

No-Downgrade Policy: The Hard Line

Axiom enforces one rule above all others. Integrity can only increase, never decrease.

The func→proc Trap

Nim strictly separates pure functions (func) and impure procedures (proc). During development, temptation strikes:

"Just one quick echo here. Let me temporarily switch to proc..."

Doesn't work in Axiom.

Why?

1. Downgrade is one-way: Once proc exists, developers keep adding side effects. It spreads like weeds.
2. Purity is binary: Either a function is pure or it isn't. "Slightly impure" is meaningless.
3. Verification requires purity: You can't mathematically prove properties about functions with unpredictable side effects.

Nim 2.0+ strictFuncs mode and effect tracking make this distinction even stronger:

# strictFuncs enforces purity at compile time
{.push strictFuncs.}
func verifyLogic(node: Node): Result[void, Error] {.raises: [], tags: [].} =
  # Compiler rejects any external state mutation or IO call
  if node.isValid: ok() else: err(InvalidNode)
{.pop.}

This is why Nim fits Axiom's architecture perfectly. The language itself enforces purity boundaries at compile time. Not just at code review.

Axiom's Enforcement Mechanism

Axiom maintains a Purity Hierarchy:

┌─────────────────────────────────────────────────────────────┐
│ Core Calculation Tier (src/core)                            │
│ ┌─────────────────────────────────────────────────────────┐ │
│ │ func-only zone: computation, parsing, normalization     │ │
│ │ Returns: Result[T], Option[T], VerifiedType[T]         │ │
│ │ Forbidden: IO, mutation, exceptions                     │ │
│ └─────────────────────────────────────────────────────────┘ │
│                                                             │
│ Boundary Executor Tier (src/ui, src/cli, gateway)          │
│ ┌─────────────────────────────────────────────────────────┐ │
│ │ proc-allowed zone: OS, TTY, filesystem, processes       │ │
│ │ Role: Execute core func results, inject dependencies    │ │
│ │ Forbidden: Business logic, domain rules                  │ │
│ └─────────────────────────────────────────────────────────┘ │
└─────────────────────────────────────────────────────────────┘

When proc shows up in src/core, it gets flagged as design debt—temporary compromise with mandatory refactor plan. Code doesn't ship until:

1. Executor boundary clearly marked
2. "func promotion" task exists in backlog
3. Impurity reason documented in CONTEXT.md

What Happens When You Violate This Rule

In Axiom, downgrading func to proc isn't just code modification. It's treated as destroying mathematical integrity. Downgrades without proper justification (CONTEXT.md update) get blocked at CI stage entirely.

Axiom's CI enforces this through Procedure Gate:

1. If src/core files change, check for proc additions
2. If func→proc conversion appears in diff, fail the commit
3. If proc exists without corresponding Boundary documentation, fail the commit

Only exception: --style-only changes (typos, comments, whitespace). Everything else needs architectural justification.

At compile time, Nim's effect system provides additional enforcement:

# [Layer 1: Core Calculation Tier]
{.push strictFuncs.}
func verifyNodeIntegrity(node: AxiomNode): Result[void, IntegrityError] {.raises: [].} =
  ## No IO, no mutation, no exceptions - mathematically pure
  if node.fingerprint == node.computedFingerprint():
    ok()
  else:
    err(IntegrityError.FingerprintMismatch)

# [Layer 2: Boundary Executor Tier]
proc executeVerification(node: AxiomNode, output: File) {.raises: [IOError].} =
  ## Thin executor: injects dependencies, delegates all logic to func
  let result = verifyNodeIntegrity(node)  # Calls pure function
  if result.isOk:
    output.write("Verification Passed\n")  # IO isolated at boundary
  else:
    output.write("Verification Failed: " & $result.error & "\n")
{.pop.}

See the pattern? verifyNodeIntegrity is pure mathematics. executeVerification is a thin wrapper handling IO. Business logic never crosses into impure territory.

Real-World Example

When implementing report rendering, Axiom faced a choice:

# Tempting initial approach:
proc renderReport(data: seq[ProofResult]) =
  # Direct IO: writes to stdout
  for r in data:
    echo r.format()

# Enforced purity approach:
func renderReportLines(data: seq[ProofResult]): seq[string] {.noSideEffect.} =
  # Pure computation: returns strings
  for r in data:
    result.add r.format()

proc writeReport(data: seq[ProofResults]) =
  # Thin executor: injects output stream
  let lines = renderReportLines(data)
  for line in lines:
    echo line

Second approach separates concerns:

• renderReportLines is pure, testable, verifiable
• writeReport is trivial executor replaceable with file output, network output, or test mock

This isn't over-engineering. It's making verification possible.

---

Why These Principles Exist

Axiom verifies AI-generated code. To do this credibly, it must be more rigorous than code it verifies.

Rule-First design ensures:

• Verification rules never get retrofitted to justify existing code
• Architecture principles are explicit, discoverable, enforced
• Integrity only moves one direction: upward

Constitution-Ordinance-Annals separation ensures:

• Principles stay visible without drowning in details
• Implementers find specifications easily
• History informs but doesn't clutter

No-Downgrade Policy ensures:

• Purity isn't sacrificed for convenience
• Verification stays mathematically sound
• Technical debt is visible, tracked, temporary

---

Conclusion

These principles aren't aspirational. CI gates, code review, architectural documentation enforce them. Every Axiom commit must pass Procedure Gate. Every proc in core must justify its existence. Every rule change must be documented before implementation.

The architecture must itself be verifiable.

Building a verification engine means you cannot verify probabilistic code with probabilistic tools. The foundation must be deterministic, mathematically proven, architecturally pure.

Next post: how Axiom transforms mathematical promises into executable proofs through bounded model checking (BMC).