# Architectural Standard: Deterministic Verification

All system design generated in this repository must strictly adhere to the "Functional Core, Imperative Shell" architecture. You must physically separate pure mathematical/business logic from external side-effects (I/O) and apply the appropriate verification tier to each layer.

## Tier 1: The Functional Core (Native Symbolic Execution / FV)
* **Definition:** Modules designated as the "Core" must be 100% pure functions. They compute data and manage state transitions but contain absolutely zero I/O, network calls, or database queries.
* **Verification Standard:** You must formally verify these pure functions using the repository's designated Native Symbolic Execution tool. Write mathematical pre/post-conditions as native code decorators/macros. The solver must prove that no valid input can ever violate these conditions across the entire state space.
* **Anti-Pattern Warning:** Do not write tautological proofs (e.g., `assert output == output`) to bypass solver timeouts. Decompose complex functions into smaller, verifiable units if the solver struggles.

## Tier 2: The Imperative Shell (DbC)
* **Definition:** Modules designated as the "Shell" handle the real world (e.g., APIs, databases, file systems). This layer is inherently non-deterministic.
* **Verification Standard:** Do not attempt formal verification here. Instead, simulate Design by Contract (DbC). Utilize strict type-state encoding and explicit invariant-checking assertions to catch malformed external payloads at the exact boundary.

## Tier 3: System Integration (PBT)
* **Definition:** The integration point where the DbC-protected Shell hands parsed data to the Formally Verified Core.
* **Verification Standard:** Validate this integration using Property-Based Testing (PBT). You must write *domain-aware*, bounded data generators. Do not generate pure garbage data; generate data structurally valid enough to bypass the initial DbC type-checks, but randomized enough to stress the internal parsers.