# Correctness / Determinism / Verification > Every principle in this category is listed as a record. Page: Ontology · Principles Canonical: https://banes-lab.com/ontology#architecture-category-correctness-determinism-verification Listed in [Ontology · Principles](https://banes-lab.com/api/pages/ontology/principles.md), after [Control / Coordination / Centralization](https://banes-lab.com/ontology/principles/architecture-category-control-coordination-centralization.md) and before [Portability / Infrastructure / Deployment](https://banes-lab.com/ontology/principles/architecture-category-portability-infrastructure-deployment.md). Every principle in this category is listed as a record. Each record carries its kind, its severity, the scopes it applies at and the layer it lives in, then the edge relations that join it to other records, the records that point back at it, the contracts that answer to it and the tensions it takes part in. The descriptors say how it is violated, detected, measured, repaired and enforced. Where the record carries one, an exemplar shows the shape before and after the principle is applied. Relations diagram The relations inside this category. ```mermaid flowchart LR n_determinism["Determinism"] n_predictability["Predictability"] n_referential_transparency["Referential Transparency"] n_pure_functions["Pure Functions"] n_immutability["Immutability"] n_reproducibility["Reproducibility"] n_repeatability["Repeatability"] n_correctness["Correctness"] n_formal_verification["Formal Verification"] n_specification_based_testing["Specification-Based Testing"] n_property_based_testing["Property-Based Testing"] n_static_analysis["Static Analysis"] n_testability["Testability"] n_validation["Validation"] n_verification["Verification"] n_determinism --> n_predictability n_determinism --> n_reproducibility n_predictability --> n_determinism n_referential_transparency --> n_pure_functions n_referential_transparency --> n_immutability n_referential_transparency --> n_determinism n_referential_transparency --> n_testability n_pure_functions --> n_testability n_pure_functions --> n_determinism n_pure_functions --> n_referential_transparency n_immutability --> n_predictability n_reproducibility --> n_determinism n_repeatability --> n_verification n_repeatability --> n_predictability n_correctness --> n_validation n_formal_verification --> n_correctness n_specification_based_testing --> n_correctness n_property_based_testing --> n_correctness n_testability --> n_pure_functions n_validation --> n_correctness n_verification --> n_correctness ``` ### Determinism - Kind: [principle](https://banes-lab.com/records/kind/principle.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - Scope: function, process, build, test - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition A design rule that the same inputs and state always produce the same result, with time and randomness passed in as inputs. Requires [Controlled State](https://banes-lab.com/records/lexicon/controlled-state.md), [Controlled State](https://banes-lab.com/records/lexicon/controlled-state.md) Reinforces [Predictability](https://banes-lab.com/records/architecture/predictability.md), [Reproducibility](https://banes-lab.com/records/architecture/reproducibility.md) Enables [Reliable Testing](https://banes-lab.com/records/lexicon/reliable-testing.md) In tension with [Runtime Adaptivity](https://banes-lab.com/records/lexicon/runtime-adaptivity.md) Conflicts with [Hidden Time/Randomness/Global State](https://banes-lab.com/records/lexicon/hidden-time-randomness-global-state.md) Referenced by [Predictability](https://banes-lab.com/records/architecture/predictability.md), [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md), [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md), [Reproducibility](https://banes-lab.com/records/architecture/reproducibility.md), [Artificial Intelligence Architecture](https://banes-lab.com/records/architecture/artificial-intelligence-architecture.md), [Agentic Architecture](https://banes-lab.com/records/architecture/agentic-architecture.md), [Write Scope and Read Population](https://banes-lab.com/records/architecture/write-scope-and-read-population.md), [One-Sided Liveness](https://banes-lab.com/records/architecture/one-sided-liveness.md), [Declare-Before-Read Order](https://banes-lab.com/records/architecture/declare-before-read-order.md), [Derived Party Count](https://banes-lab.com/records/architecture/derived-party-count.md), [Externally Resolved Slot](https://banes-lab.com/records/architecture/externally-resolved-slot.md) Contracts [Computation Core](https://banes-lab.com/records/algorithms/computation-core.md) Tensions [Determinism / Runtime Adaptivity](https://banes-lab.com/records/tension/determinism-runtime-adaptivity.md) Distinct from [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md): Determinism is the same inputs giving the same result, while referential transparency is being able to replace an expression by its value. Violated by nondeterministic behavior without explicit source Detected by flaky tests, hidden random/time calls Measured by flake rate, reproducibility score Refactored by Inject Clock/RNG, Control State Enforced by deterministic test rules Before ```typescript function makeFoo(name: string) { return { id: crypto.randomUUID(), name, createdAt: new Date() }; } ``` After ```typescript function makeFoo(name: string, id: FooId, createdAt: Date): Foo { return { id, name, createdAt }; } ``` How it is checked Checked by deterministic test rules Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Controlled State](https://banes-lab.com/records/lexicon/controlled-state.md), [Controlled State](https://banes-lab.com/records/lexicon/controlled-state.md), [Predictability](https://banes-lab.com/records/architecture/predictability.md), [Reproducibility](https://banes-lab.com/records/architecture/reproducibility.md), [Reliable Testing](https://banes-lab.com/records/lexicon/reliable-testing.md) Shape it refuses [Hidden Time/Randomness/Global State](https://banes-lab.com/records/lexicon/hidden-time-randomness-global-state.md) ### Predictability - Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - Scope: API, module, runtime - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The degree to which a caller can foresee what an operation does from its interface and contract. Requires [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Explicit Contracts](https://banes-lab.com/records/architecture/explicit-contracts.md) Reinforces [Principle of Least Surprise](https://banes-lab.com/records/architecture/principle-of-least-surprise.md) Enables [Safe Refactoring](https://banes-lab.com/records/lexicon/safe-refactoring.md) In tension with [Dynamic Runtime Behavior](https://banes-lab.com/records/lexicon/dynamic-runtime-behavior.md) Conflicts with [Hidden Behavior](https://banes-lab.com/records/lexicon/hidden-behavior.md) Referenced by [Runtime Discovery](https://banes-lab.com/records/architecture/runtime-discovery.md), [Dynamic Binding](https://banes-lab.com/records/architecture/dynamic-binding.md), [Runtime Extensibility](https://banes-lab.com/records/architecture/runtime-extensibility.md), [Design by Contract](https://banes-lab.com/records/architecture/design-by-contract.md), [Explicit Contracts](https://banes-lab.com/records/architecture/explicit-contracts.md), [API Contract](https://banes-lab.com/records/architecture/api-contract.md), [Postconditions](https://banes-lab.com/records/architecture/postconditions.md), [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Immutability](https://banes-lab.com/records/architecture/immutability.md), [Repeatability](https://banes-lab.com/records/architecture/repeatability.md), [Pattern Consistency](https://banes-lab.com/records/architecture/pattern-consistency.md), [Declarative Configuration](https://banes-lab.com/records/architecture/declarative-configuration.md), [Convention over Configuration](https://banes-lab.com/records/architecture/convention-over-configuration.md), [Principle of Least Surprise](https://banes-lab.com/records/architecture/principle-of-least-surprise.md), [State Isolation](https://banes-lab.com/records/architecture/state-isolation.md), [Controlled Side Effects](https://banes-lab.com/records/architecture/controlled-side-effects.md) Tensions [Predictability / Dynamic Runtime Behavior](https://banes-lab.com/records/tension/dynamic-runtime-behavior-predictability.md) Distinct from [Correctness](https://banes-lab.com/records/architecture/correctness.md): Predictability is foreseeing behavior from the contract, while correctness is the behavior matching its specification. Distinct from [Pattern Consistency](https://banes-lab.com/records/architecture/pattern-consistency.md): Predictability is foreseeing one operation, while pattern consistency is one problem solved one way across the codebase. Distinct from [Interoperability](https://banes-lab.com/records/architecture/interoperability.md): Predictability is a caller foreseeing behavior, while interoperability is systems exchanging data. Distinct from [Reproducibility](https://banes-lab.com/records/architecture/reproducibility.md): Predictability is foreseeing what an operation does, while reproducibility is a run giving the same output from pinned inputs on another machine. Distinct from [Testability](https://banes-lab.com/records/architecture/testability.md): Predictability is foreseeing behavior, while testability is exercising code in isolation. Distinct from [Concurrency Correctness](https://banes-lab.com/records/lexicon/concurrency-correctness.md): Predictability is foreseeing behavior from a contract, while concurrency correctness is freedom from races when units run at once. Distinct from [Dynamic Runtime Behavior](https://banes-lab.com/records/lexicon/dynamic-runtime-behavior.md): Predictability is foreseeable behavior, while dynamic runtime behavior is the adaptivity that undermines it. Distinct from [Maintainability](https://banes-lab.com/records/lexicon/maintainability.md): Predictability is foreseeing behavior, while maintainability is the ease of changing it. Distinct from [Security](https://banes-lab.com/records/lexicon/security.md): Predictability is foreseeable behavior, while security is protection from misuse. Distinct from [Startup Cost](https://banes-lab.com/records/lexicon/startup-cost.md): Predictability is foreseeable behavior, while startup cost is the time discovery adds at initialization. Distinct from [Repeatability](https://banes-lab.com/records/architecture/repeatability.md): Predictability is foreseeing an outcome from the contract, while repeatability is rerunning and observing the same outcome. Distinct from [Runtime Extensibility](https://banes-lab.com/records/architecture/runtime-extensibility.md): Predictability is fixed, foreseeable behavior, while runtime extensibility is adding capability to a running system. Distinct from [Static Safety](https://banes-lab.com/records/lexicon/static-safety.md): Predictability is a caller foreseeing behavior, while static safety is the compiler catching classes of error before the code runs. Distinct from [Thread Safety](https://banes-lab.com/records/lexicon/thread-safety.md): Predictability is foreseeing behavior from a contract, while thread safety is data surviving concurrent access uncorrupted. Violated by surprising side effects, implicit ordering Detected by nondeterministic tests, ambiguous APIs Measured by flake/misuse rate Refactored by Make Behavior Explicit, Add Contracts Enforced by [tests](https://banes-lab.com/records/lexicon/tests.md), [contracts](https://banes-lab.com/records/lexicon/contracts.md), linting Before ```typescript function saveFoo(foo: Foo) { if (Math.random() > 0.5) return memoryStore.save(foo); return sqlStore.save(foo); } ``` After ```typescript function saveFoo(store: FooStore, foo: Foo) { return store.save(foo); } ``` How it is checked Checked by tests, contracts, linting Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Explicit Contracts](https://banes-lab.com/records/architecture/explicit-contracts.md), [Principle of Least Surprise](https://banes-lab.com/records/architecture/principle-of-least-surprise.md), [Safe Refactoring](https://banes-lab.com/records/lexicon/safe-refactoring.md) Shape it refuses [Hidden Behavior](https://banes-lab.com/records/lexicon/hidden-behavior.md) ### Referential Transparency - Kind: [principle](https://banes-lab.com/records/kind/principle.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [contextual](https://banes-lab.com/records/vocabulary/severity-contextual.md) - Scope: function, expression - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition A design rule that an expression can be replaced by its value without changing the program's behavior. Requires [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md), [Immutability](https://banes-lab.com/records/architecture/immutability.md) Reinforces [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Testability](https://banes-lab.com/records/architecture/testability.md) Enables [Safe Substitution](https://banes-lab.com/records/lexicon/safe-substitution.md) In tension with [Stateful IO](https://banes-lab.com/records/lexicon/stateful-io.md) Conflicts with [Side Effects](https://banes-lab.com/records/lexicon/side-effects.md) Referenced by [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md) Tensions [Referential Transparency / Stateful IO](https://banes-lab.com/records/tension/referential-transparency-stateful-io.md) Distinct from [Immutability](https://banes-lab.com/records/architecture/immutability.md): Referential transparency lets an expression be replaced by its value, while immutability forbids a value from changing after creation. Violated by same input producing different output Detected by hidden dependency on time/random/global state Measured by pure function coverage Refactored by Extract Pure Function, Inject Dependency Enforced by [code review](https://banes-lab.com/records/architecture/code-review.md), functional boundaries Before ```typescript function fooTotal(values: number[]) { globalCounter += 1; return values.reduce((a, b) => a + b, 0) + globalCounter; } ``` After ```typescript function fooTotal(values: readonly number[]) { return values.reduce((a, b) => a + b, 0); } ``` How it is checked Checked by code review, functional boundaries Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md), [Immutability](https://banes-lab.com/records/architecture/immutability.md), [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Testability](https://banes-lab.com/records/architecture/testability.md), [Safe Substitution](https://banes-lab.com/records/lexicon/safe-substitution.md) Shape it refuses [Side Effects](https://banes-lab.com/records/lexicon/side-effects.md) ### Pure Functions - Kind: [technique](https://banes-lab.com/records/kind/technique.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - Scope: function, domain logic - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition A technique for writing logic as functions whose result depends only on their arguments and which have no side effects. Requires [No Side Effects](https://banes-lab.com/records/lexicon/no-side-effects.md), [Explicit Inputs](https://banes-lab.com/records/lexicon/explicit-inputs.md) Reinforces [Testability](https://banes-lab.com/records/architecture/testability.md), [Determinism](https://banes-lab.com/records/architecture/determinism.md) Enables [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md) In tension with [Stateful Operations](https://banes-lab.com/records/lexicon/stateful-operations.md) Conflicts with [Hidden IO](https://banes-lab.com/records/lexicon/hidden-io.md) Referenced by [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md), [Testability](https://banes-lab.com/records/architecture/testability.md) Tensions [Pure Functions / Stateful Operations](https://banes-lab.com/records/tension/pure-functions-stateful-operations.md) Violated by mutation, IO, global reads/writes Detected by side-effect calls inside pure layer Measured by pure core ratio Refactored by Extract Pure Logic, Move IO Outward Enforced by layer rules, [tests](https://banes-lab.com/records/lexicon/tests.md) Before ```typescript function normalizeFoo(foo: Foo) { foo.name = foo.name.trim(); fooStore.save(foo); return foo; } ``` After ```typescript function normalizeFoo(foo: Foo): Foo { return { ...foo, name: foo.name.trim() }; } ``` How it is checked Checked by layer rules, tests Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [No Side Effects](https://banes-lab.com/records/lexicon/no-side-effects.md), [Explicit Inputs](https://banes-lab.com/records/lexicon/explicit-inputs.md), [Testability](https://banes-lab.com/records/architecture/testability.md), [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md) Shape it refuses [Hidden IO](https://banes-lab.com/records/lexicon/hidden-io.md) ### Immutability - Kind: [principle](https://banes-lab.com/records/kind/principle.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - Scope: data, value object, concurrency - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition A design rule that a value is never changed after it is created, and a change produces a new value. Requires [Value Semantics](https://banes-lab.com/records/lexicon/value-semantics.md) Reinforces [Thread Safety](https://banes-lab.com/records/lexicon/thread-safety.md), [Predictability](https://banes-lab.com/records/architecture/predictability.md) Enables [Safe Sharing](https://banes-lab.com/records/lexicon/safe-sharing.md) In tension with [Allocation Cost](https://banes-lab.com/records/lexicon/allocation-cost.md) Conflicts with [Shared Mutable State](https://banes-lab.com/records/architecture/shared-mutable-state.md) Referenced by [Value Object](https://banes-lab.com/records/architecture/value-object.md), [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md), [Independent Lifetime Axes](https://banes-lab.com/records/architecture/independent-lifetime-axes.md) Tensions [Immutability / Allocation Cost](https://banes-lab.com/records/tension/allocation-cost-immutability.md) Violated by mutating value objects, exposed mutable collections Detected by setters on value objects, mutable public fields Measured by mutable state count Refactored by Make Immutable, Copy-on-Write Enforced by type system, lint rules Refused by rules immutability Before ```typescript type Foo = { name: string; tags: string[] }; function addTag(foo: Foo, tag: string) { foo.tags.push(tag); return foo; } ``` After ```typescript type Foo = Readonly<{ name: string; tags: readonly string[] }>; function addTag(foo: Foo, tag: string): Foo { return { ...foo, tags: [...foo.tags, tag] }; } ``` How it is checked Checked by type system, lint rules Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Value Semantics](https://banes-lab.com/records/lexicon/value-semantics.md), [Thread Safety](https://banes-lab.com/records/lexicon/thread-safety.md), [Predictability](https://banes-lab.com/records/architecture/predictability.md), [Safe Sharing](https://banes-lab.com/records/lexicon/safe-sharing.md) Shape it refuses [Shared Mutable State](https://banes-lab.com/records/architecture/shared-mutable-state.md) ### Reproducibility - Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - Scope: build, test, deployment, ML - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The degree to which a build, test or training run gives the same output from the same pinned inputs on another machine. Requires [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Versioned Inputs](https://banes-lab.com/records/lexicon/versioned-inputs.md) Reinforces [Auditability](https://banes-lab.com/records/architecture/auditability.md) Enables [Debugging](https://banes-lab.com/records/lexicon/debugging.md), [Compliance](https://banes-lab.com/records/architecture/compliance.md) In tension with [Continuous Updates](https://banes-lab.com/records/lexicon/continuous-updates.md) Conflicts with [Floating Dependencies](https://banes-lab.com/records/lexicon/floating-dependencies.md), [Flaky Test Normalization](https://banes-lab.com/records/architecture/flaky-test-normalization.md) Referenced by [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Environment Parity](https://banes-lab.com/records/architecture/environment-parity.md), [Infrastructure as Code](https://banes-lab.com/records/architecture/infrastructure-as-code.md), [Immutable Infrastructure](https://banes-lab.com/records/architecture/immutable-infrastructure.md), [Machine Learning Architecture](https://banes-lab.com/records/architecture/machine-learning-architecture.md), [Prompt Engineering](https://banes-lab.com/records/architecture/prompt-engineering.md), [Benchmarking](https://banes-lab.com/records/architecture/benchmarking.md) Tensions [Reproducibility / Continuous Updates](https://banes-lab.com/records/tension/continuous-updates-reproducibility.md) Distinct from [Continuous Updates](https://banes-lab.com/records/lexicon/continuous-updates.md): Reproducibility pins every input, while continuous updates are the dependency changes that pinning holds back. Violated by unpinned dependencies, nondeterministic builds Detected by build output drift Measured by reproducible build/test pass rate Refactored by Pin Versions, Lock Inputs, Capture Environment Enforced by lockfiles, build verification Before ```typescript const result = trainFoo(data, { seed: Math.random() }); ``` After ```typescript const config = { seed: 42, datasetVersion: "foo-v3", algorithmVersion: "1.2.0" } as const; const result = trainFoo(data, config); ``` How it is checked Checked by lockfiles, build verification Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Determinism](https://banes-lab.com/records/architecture/determinism.md), [Versioned Inputs](https://banes-lab.com/records/lexicon/versioned-inputs.md), [Auditability](https://banes-lab.com/records/architecture/auditability.md), [Debugging](https://banes-lab.com/records/lexicon/debugging.md), [Compliance](https://banes-lab.com/records/architecture/compliance.md) Shape it refuses [Floating Dependencies](https://banes-lab.com/records/lexicon/floating-dependencies.md), [Flaky Test Normalization](https://banes-lab.com/records/architecture/flaky-test-normalization.md) ### Repeatability - Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [mandatory](https://banes-lab.com/records/vocabulary/severity-mandatory.md) - Scope: test, build, process - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The degree to which rerunning the same test or process in the same environment gives the same result. Requires [Controlled State](https://banes-lab.com/records/lexicon/controlled-state.md) Reinforces [Verification](https://banes-lab.com/records/architecture/verification.md), [Predictability](https://banes-lab.com/records/architecture/predictability.md) Enables [Reliable Automation](https://banes-lab.com/records/lexicon/reliable-automation.md) In tension with [Real-World Variability](https://banes-lab.com/records/lexicon/real-world-variability.md) Conflicts with [Environment-Sensitive Behavior](https://banes-lab.com/records/lexicon/environment-sensitive-behavior.md) Tensions [Repeatability / Real-World Variability](https://banes-lab.com/records/tension/real-world-variability-repeatability.md) Distinct from [Real-World Variability](https://banes-lab.com/records/lexicon/real-world-variability.md): Repeatability is the same result from a controlled rerun, while real-world variability is how far those controlled conditions differ from production. Violated by tests depending on ordering/time/external state Detected by flaky test results Measured by rerun consistency Refactored by Isolate Environment, Mock External Inputs Enforced by CI rerun policy Before ```typescript test("foo", () => expect(runFoo(Date.now())).toEqual(snapshot())); ``` After ```typescript test("foo", () => { const clock = new FixedClock("2026-01-01T00:00:00Z"); expect(runFoo(clock)).toEqual(expectedFoo); }); ``` How it is checked Checked by CI rerun policy Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Controlled State](https://banes-lab.com/records/lexicon/controlled-state.md), [Verification](https://banes-lab.com/records/architecture/verification.md), [Predictability](https://banes-lab.com/records/architecture/predictability.md), [Reliable Automation](https://banes-lab.com/records/lexicon/reliable-automation.md) Shape it refuses [Environment-Sensitive Behavior](https://banes-lab.com/records/lexicon/environment-sensitive-behavior.md) ### Correctness - Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [mandatory](https://banes-lab.com/records/vocabulary/severity-mandatory.md) - Scope: function, module, system - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The degree to which the behavior of code matches its specification. Requires [Specification](https://banes-lab.com/records/lexicon/specification.md), [Validation](https://banes-lab.com/records/architecture/validation.md), [Tests](https://banes-lab.com/records/lexicon/tests.md) Reinforces [Design by Contract](https://banes-lab.com/records/architecture/design-by-contract.md) Enables [Safe Operation](https://banes-lab.com/records/lexicon/safe-operation.md) In tension with [Delivery Speed](https://banes-lab.com/records/lexicon/delivery-speed.md) Conflicts with [Undefined Behavior](https://banes-lab.com/records/lexicon/undefined-behavior.md) Referenced by [Domain Model](https://banes-lab.com/records/architecture/domain-model.md), [Happens-Before Relationship](https://banes-lab.com/records/architecture/happens-before-relationship.md), [Design by Contract](https://banes-lab.com/records/architecture/design-by-contract.md), [Semantic Contracts](https://banes-lab.com/records/architecture/semantic-contracts.md), [Preconditions](https://banes-lab.com/records/architecture/preconditions.md), [Postconditions](https://banes-lab.com/records/architecture/postconditions.md), [Invariant](https://banes-lab.com/records/architecture/invariant.md), [Formal Verification](https://banes-lab.com/records/architecture/formal-verification.md), [Specification-Based Testing](https://banes-lab.com/records/architecture/specification-based-testing.md), [Property-Based Testing](https://banes-lab.com/records/architecture/property-based-testing.md), [Validation](https://banes-lab.com/records/architecture/validation.md), [Verification](https://banes-lab.com/records/architecture/verification.md), [Fail Fast](https://banes-lab.com/records/architecture/fail-fast.md), [Error Handling](https://banes-lab.com/records/architecture/error-handling.md), [Design Review](https://banes-lab.com/records/architecture/design-review.md), [First-Principles Design](https://banes-lab.com/records/architecture/first-principles-design.md), [Model Evaluation](https://banes-lab.com/records/architecture/model-evaluation.md), [Finite State Machine](https://banes-lab.com/records/architecture/finite-state-machine.md), [Schema Validation](https://banes-lab.com/records/architecture/schema-validation.md), [Type Safety](https://banes-lab.com/records/architecture/type-safety.md), [Single Source of Truth](https://banes-lab.com/records/architecture/single-source-of-truth.md), [Semantic Consistency](https://banes-lab.com/records/architecture/semantic-consistency.md), [Input Validation](https://banes-lab.com/records/architecture/input-validation.md), [Atomicity](https://banes-lab.com/records/architecture/atomicity.md), [ACID](https://banes-lab.com/records/architecture/acid.md), [Consistency](https://banes-lab.com/records/architecture/consistency.md), [Isolation](https://banes-lab.com/records/architecture/isolation.md), [Concurrency Control](https://banes-lab.com/records/architecture/concurrency-control.md) Tensions [Correctness / Delivery Speed](https://banes-lab.com/records/tension/correctness-delivery-speed.md) Distinct from [Interoperability](https://banes-lab.com/records/architecture/interoperability.md): Correctness is code matching its specification, while interoperability is separate systems exchanging data correctly. Distinct from [Observability](https://banes-lab.com/records/architecture/observability.md): Correctness is matching the specification, while observability is inferring behavior from the signals a system emits. Distinct from [Maintainability](https://banes-lab.com/records/lexicon/maintainability.md): Correctness is behaving as specified now, while maintainability is the ease of changing the behavior later. Distinct from [Robustness](https://banes-lab.com/records/lexicon/robustness.md): Correctness is behaving as specified for valid input, while robustness is continuing to operate under invalid input and stress. Distinct from [Simplicity](https://banes-lab.com/records/lexicon/simplicity.md): Correctness is matching the specification, while simplicity is the absence of unneeded structure. Distinct from [Model Safety](https://banes-lab.com/records/architecture/model-safety.md): Correctness is matching a specification, while model safety is preventing harmful model inputs, outputs and actions. Distinct from [Resilience](https://banes-lab.com/records/architecture/resilience.md): Correctness is right behavior, while resilience is containing failure and recovering from it. Distinct from [Semantic Consistency](https://banes-lab.com/records/architecture/semantic-consistency.md): Correctness is behavior matching the specification, while semantic consistency is one name keeping one meaning. Distinct from [Security](https://banes-lab.com/records/lexicon/security.md): Correctness is matching the specification, while security is protecting data and behavior from misuse. Violated by behavior diverging from specification Detected by failing tests, invariant violations Measured by defect rate, spec coverage Refactored by Add Tests, Fix Logic, Add Contracts Enforced by CI, formal/static checks Before ```typescript function averageFoo(total: number, count: number) { return total / count; } ``` After ```typescript function averageFoo(total: number, count: number) { if (!Number.isFinite(total)) throw new Error("invalid total"); if (!Number.isInteger(count) || count <= 0) throw new Error("invalid count"); return total / count; } ``` How it is checked Checked by CI, formal/static checks Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Specification](https://banes-lab.com/records/lexicon/specification.md), [Validation](https://banes-lab.com/records/architecture/validation.md), [Tests](https://banes-lab.com/records/lexicon/tests.md), [Design by Contract](https://banes-lab.com/records/architecture/design-by-contract.md), [Safe Operation](https://banes-lab.com/records/lexicon/safe-operation.md) Shape it refuses [Undefined Behavior](https://banes-lab.com/records/lexicon/undefined-behavior.md) ### Formal Verification - Kind: [activity](https://banes-lab.com/records/kind/activity.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [contextual](https://banes-lab.com/records/vocabulary/severity-contextual.md) - Scope: algorithm, protocol, critical system - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The activity of proving, against a formal specification, that an algorithm or protocol keeps its invariants for every input. Requires [Formal Specification](https://banes-lab.com/records/lexicon/formal-specification.md) Reinforces [Correctness](https://banes-lab.com/records/architecture/correctness.md) Enables [Mathematical Assurance](https://banes-lab.com/records/lexicon/mathematical-assurance.md) In tension with [Cost/Complexity](https://banes-lab.com/records/lexicon/cost-complexity.md) Conflicts with [Informal Validation Only](https://banes-lab.com/records/lexicon/informal-validation-only.md) Tensions [Formal Verification / Cost/Complexity](https://banes-lab.com/records/tension/cost-complexity-formal-verification.md) Violated by critical logic without proof where required Detected by missing formal model for critical invariant Measured by proven property coverage Refactored by Specify Model, Prove Invariant Enforced by proof tooling Before ```typescript function transferFoo(a: FooBalance, b: FooBalance, amount: number) { a.value -= amount; b.value += amount; } ``` After ```typescript function transferFoo(state: FooState, amount: PositiveAmount): FooState { requires(state.from >= amount.value); const next = { from: state.from - amount.value, to: state.to + amount.value }; ensures(next.from + next.to === state.from + state.to); return next; } ``` How it is checked Checked by proof tooling Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Formal Specification](https://banes-lab.com/records/lexicon/formal-specification.md), [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Mathematical Assurance](https://banes-lab.com/records/lexicon/mathematical-assurance.md) Shape it refuses [Informal Validation Only](https://banes-lab.com/records/lexicon/informal-validation-only.md) ### Specification-Based Testing - Kind: [activity](https://banes-lab.com/records/kind/activity.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - Scope: function, API, module - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The activity of deriving tests from a specification's stated behavior, independently of how the code implements it. Requires [Specification](https://banes-lab.com/records/lexicon/specification.md) Reinforces [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Contracts](https://banes-lab.com/records/lexicon/contracts.md) Enables [Behavior Validation](https://banes-lab.com/records/lexicon/behavior-validation.md) In tension with [Spec Maintenance](https://banes-lab.com/records/lexicon/spec-maintenance.md) Conflicts with [Implementation-Only Testing](https://banes-lab.com/records/lexicon/implementation-only-testing.md), [Mock Mirage](https://banes-lab.com/records/architecture/mock-mirage.md) Contracts [Test Coverage Kernel](https://banes-lab.com/records/algorithms/test-coverage-kernel.md) Tensions [Specification-Based Testing / Spec Maintenance](https://banes-lab.com/records/tension/spec-maintenance-specification-based-testing.md) Violated by tests coupled to implementation details Detected by lack of spec-derived tests Measured by spec coverage Refactored by Add Spec Tests Enforced by test gates Before ```typescript test("saveFoo", async () => expect(await saveFoo(foo)).toBeTruthy()); ``` After ```typescript describeContract("FooStore", store => { it("returns the saved Foo", async () => { await store.save(foo); expect(await store.find(foo.id)).toEqual(foo); }); }); ``` How it is checked Checked by test gates Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Specification](https://banes-lab.com/records/lexicon/specification.md), [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Contracts](https://banes-lab.com/records/lexicon/contracts.md), [Behavior Validation](https://banes-lab.com/records/lexicon/behavior-validation.md) Shape it refuses [Implementation-Only Testing](https://banes-lab.com/records/lexicon/implementation-only-testing.md), [Mock Mirage](https://banes-lab.com/records/architecture/mock-mirage.md) ### Property-Based Testing - Kind: [activity](https://banes-lab.com/records/kind/activity.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - Scope: function, algorithm, parser, domain invariant - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The activity of checking that a stated property holds for many generated inputs, and shrinking each failure to a minimal counterexample. Requires [Properties/Invariants](https://banes-lab.com/records/lexicon/properties-invariants.md) Reinforces [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Robustness](https://banes-lab.com/records/lexicon/robustness.md) Enables [Broad Input Exploration](https://banes-lab.com/records/lexicon/broad-input-exploration.md) In tension with [Shrinking/Debug Complexity](https://banes-lab.com/records/lexicon/shrinking-debug-complexity.md) Conflicts with [Example-Only Testing](https://banes-lab.com/records/lexicon/example-only-testing.md) Tensions [Property-Based Testing / Shrinking/Debug Complexity](https://banes-lab.com/records/tension/property-based-testing-shrinking-debug-complexity.md) Violated by invariant-heavy code with only example tests Detected by missing generative tests for critical properties Measured by property coverage, counterexample count Refactored by Define Property, Add Generator Enforced by property test suite Before ```typescript test("normalizeFoo", () => expect(normalizeFoo({ name: " Foo " }).name).toBe("Foo")); ``` After ```typescript property(string(), name => { const once = normalizeFoo({ name }); const twice = normalizeFoo(once); expect(twice).toEqual(once); }); ``` How it is checked Checked by property test suite Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Properties/Invariants](https://banes-lab.com/records/lexicon/properties-invariants.md), [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Robustness](https://banes-lab.com/records/lexicon/robustness.md), [Broad Input Exploration](https://banes-lab.com/records/lexicon/broad-input-exploration.md) Shape it refuses [Example-Only Testing](https://banes-lab.com/records/lexicon/example-only-testing.md) ### Static Analysis - Kind: [mechanism](https://banes-lab.com/records/kind/mechanism.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [mandatory](https://banes-lab.com/records/vocabulary/severity-mandatory.md) - Scope: codebase, build - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition A mechanism that checks source code against a ruleset without running it. Requires [Ruleset](https://banes-lab.com/records/lexicon/ruleset.md) Reinforces [Type Safety](https://banes-lab.com/records/architecture/type-safety.md), [Security](https://banes-lab.com/records/lexicon/security.md), [Architecture Compliance](https://banes-lab.com/records/lexicon/architecture-compliance.md) Enables [Automated Enforcement](https://banes-lab.com/records/lexicon/automated-enforcement.md) In tension with [False Positives](https://banes-lab.com/records/lexicon/false-positives.md) Conflicts with [Unchecked Dynamic Code](https://banes-lab.com/records/lexicon/unchecked-dynamic-code.md) Referenced by [Runtime Discovery](https://banes-lab.com/records/architecture/runtime-discovery.md), [Metaprogramming](https://banes-lab.com/records/architecture/metaprogramming.md), [Reflection](https://banes-lab.com/records/architecture/reflection.md), [Plugin Architecture](https://banes-lab.com/records/architecture/plugin-architecture.md), [Type Safety](https://banes-lab.com/records/architecture/type-safety.md) Tensions [Static Analysis / False Positives](https://banes-lab.com/records/tension/false-positives-static-analysis.md) Distinct from [Type Safety](https://banes-lab.com/records/architecture/type-safety.md): Static analysis checks source against any ruleset, while type safety is the compiler rejecting operations on values of the wrong type. Distinct from [Automated Enforcement](https://banes-lab.com/records/lexicon/automated-enforcement.md): Static analysis is one way to check source without running it, while automated enforcement is any machine check that rules hold. Violated by ignored analyzer findings Detected by static analysis rule failures Measured by issue count, false-positive rate Refactored by Fix Violations, Tune Rules Enforced by CI quality gates Before ```typescript const foo: any = loadFoo(); foo.nmae.toUpperCase(); ``` After ```typescript const foo: Foo = loadFoo(); foo.name.toUpperCase(); runTypeCheck({ noImplicitAny: true, strictNullChecks: true }); ``` How it is checked Checked by CI quality gates Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Ruleset](https://banes-lab.com/records/lexicon/ruleset.md), [Type Safety](https://banes-lab.com/records/architecture/type-safety.md), [Security](https://banes-lab.com/records/lexicon/security.md), [Architecture Compliance](https://banes-lab.com/records/lexicon/architecture-compliance.md), [Automated Enforcement](https://banes-lab.com/records/lexicon/automated-enforcement.md) Shape it refuses [Unchecked Dynamic Code](https://banes-lab.com/records/lexicon/unchecked-dynamic-code.md) ### Testability - Kind: [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [mandatory](https://banes-lab.com/records/vocabulary/severity-mandatory.md) - Scope: class, module, service - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The degree to which code can be tested in isolation, with its dependencies, time and randomness supplied by the test. Requires [Low Coupling](https://banes-lab.com/records/architecture/low-coupling.md), [Deterministic Behavior](https://banes-lab.com/records/lexicon/deterministic-behavior.md) Reinforces [Dependency Inversion Principle (DIP)](https://banes-lab.com/records/architecture/dependency-inversion.md), [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md) Enables [Regression Safety](https://banes-lab.com/records/lexicon/regression-safety.md) In tension with [Encapsulation Extremes](https://banes-lab.com/records/lexicon/encapsulation-extremes.md) Conflicts with [Hidden Dependencies](https://banes-lab.com/records/lexicon/hidden-dependencies.md), [Test Pyramid Inversion](https://banes-lab.com/records/architecture/test-pyramid-inversion.md) Referenced by [Interface-Based Design](https://banes-lab.com/records/architecture/interface-based-design.md), [Postconditions](https://banes-lab.com/records/architecture/postconditions.md), [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md), [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md), [Single Responsibility Principle (SRP)](https://banes-lab.com/records/architecture/single-responsibility.md), [High Cohesion](https://banes-lab.com/records/architecture/high-cohesion.md), [Singleton Pattern](https://banes-lab.com/records/architecture/singleton-pattern.md), [Stateless Processing](https://banes-lab.com/records/architecture/stateless-processing.md), [Dependency Injection](https://banes-lab.com/records/architecture/dependency-injection.md), [Service Locator Pattern](https://banes-lab.com/records/architecture/service-locator-pattern.md), [Ports and Adapters Architecture](https://banes-lab.com/records/architecture/ports-and-adapters-architecture.md), [Hexagonal Architecture](https://banes-lab.com/records/architecture/hexagonal-architecture.md), [Clean Architecture](https://banes-lab.com/records/architecture/clean-architecture.md), [State Isolation](https://banes-lab.com/records/architecture/state-isolation.md), [Controlled Side Effects](https://banes-lab.com/records/architecture/controlled-side-effects.md) Tensions [Testability / Encapsulation Extremes](https://banes-lab.com/records/tension/encapsulation-extremes-testability.md) Distinct from [High Cohesion](https://banes-lab.com/records/architecture/high-cohesion.md): Testability is running code in isolation, while high cohesion is its members sharing one purpose. Distinct from [Encapsulation Extremes](https://banes-lab.com/records/lexicon/encapsulation-extremes.md): Testability is observing a unit in a test, while encapsulation extremes are the hiding that makes it hard to observe. Distinct from [Explicit Dependencies](https://banes-lab.com/records/lexicon/explicit-dependencies.md): Testability is supplying a unit's dependencies in a test, while explicit dependencies are those dependencies being visible in its signature. Violated by hardcoded dependencies, [global state](https://banes-lab.com/records/lexicon/global-state.md), nondeterminism Detected by difficult setup, excessive mocking, flaky tests Measured by test setup complexity, coverage, flake rate Refactored by Inject Dependencies, Isolate Side Effects Enforced by test gates, [architecture review](https://banes-lab.com/records/architecture/architecture-review.md) Before ```typescript function createFoo(name: string) { return fooDb.save({ id: crypto.randomUUID(), name, createdAt: new Date() }); } ``` After ```typescript function createFoo(name: string, ids: IdSource, clock: Clock, store: FooStore) { return store.save({ id: ids.nextFooId(), name, createdAt: clock.now() }); } ``` How it is checked Checked by test gates, architecture review Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Low Coupling](https://banes-lab.com/records/architecture/low-coupling.md), [Deterministic Behavior](https://banes-lab.com/records/lexicon/deterministic-behavior.md), [Dependency Inversion Principle (DIP)](https://banes-lab.com/records/architecture/dependency-inversion.md), [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md), [Regression Safety](https://banes-lab.com/records/lexicon/regression-safety.md) Shape it refuses [Hidden Dependencies](https://banes-lab.com/records/lexicon/hidden-dependencies.md), [Test Pyramid Inversion](https://banes-lab.com/records/architecture/test-pyramid-inversion.md) ### Validation - Kind: [activity](https://banes-lab.com/records/kind/activity.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [mandatory](https://banes-lab.com/records/vocabulary/severity-mandatory.md) - Scope: input, behavior, requirement - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The activity of checking that inputs and delivered behavior meet the acceptance criteria of their users. Requires [Acceptance Criteria](https://banes-lab.com/records/lexicon/acceptance-criteria.md) Reinforces [Correctness](https://banes-lab.com/records/architecture/correctness.md) Enables [Fitness for Use](https://banes-lab.com/records/lexicon/fitness-for-use.md) In tension with [Iteration Speed](https://banes-lab.com/records/lexicon/iteration-speed.md) Conflicts with [Assumption-Driven Delivery](https://banes-lab.com/records/lexicon/assumption-driven-delivery.md) Referenced by [Invariant](https://banes-lab.com/records/architecture/invariant.md), [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Fail Fast](https://banes-lab.com/records/architecture/fail-fast.md), [Self-Describing Structures](https://banes-lab.com/records/architecture/self-describing-structures.md), [Metadata-Driven Design](https://banes-lab.com/records/architecture/metadata-driven-design.md), [Canonicalization](https://banes-lab.com/records/architecture/canonicalization.md), [Consistency](https://banes-lab.com/records/architecture/consistency.md) Tensions [Validation / Iteration Speed](https://banes-lab.com/records/tension/iteration-speed-validation.md) Violated by unvalidated user/system assumptions Detected by missing acceptance tests Measured by acceptance coverage Refactored by Add Validation Rules, Add Acceptance Tests Enforced by CI gates, QA policy Before ```typescript function createFoo(input: any) { return fooStore.save(input); } ``` After ```typescript function createFoo(input: unknown) { const foo = CreateFooSchema.parse(input); return fooStore.save(foo); } ``` How it is checked Checked by CI gates, QA policy Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Acceptance Criteria](https://banes-lab.com/records/lexicon/acceptance-criteria.md), [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Fitness for Use](https://banes-lab.com/records/lexicon/fitness-for-use.md) Shape it refuses [Assumption-Driven Delivery](https://banes-lab.com/records/lexicon/assumption-driven-delivery.md) ### Verification - Kind: [activity](https://banes-lab.com/records/kind/activity.md) - Category: [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md) - Severity: [mandatory](https://banes-lab.com/records/vocabulary/severity-mandatory.md) - Scope: implementation, system - Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md) Details Definition The activity of checking that an implementation conforms to its specification. Requires [Specification](https://banes-lab.com/records/lexicon/specification.md) Reinforces [Correctness](https://banes-lab.com/records/architecture/correctness.md) Enables [Specification Compliance](https://banes-lab.com/records/lexicon/specification-compliance.md) In tension with [Cost](https://banes-lab.com/records/lexicon/cost.md) Conflicts with [Untested Implementation](https://banes-lab.com/records/lexicon/untested-implementation.md) Referenced by [Repeatability](https://banes-lab.com/records/architecture/repeatability.md) Contracts [Codebase Verification Kernel](https://banes-lab.com/records/algorithms/codebase-verification-kernel.md) Tensions [Verification / Cost](https://banes-lab.com/records/tension/cost-verification.md) Violated by code lacking spec conformance checks Detected by missing tests/static checks Measured by verification coverage Refactored by Add Tests, Add Static Checks Enforced by CI gates Before ```typescript await fooStore.save(foo); return { ok: true }; ``` After ```typescript await fooStore.save(foo); const persisted = await fooStore.find(foo.id); if (!persisted || persisted.version !== foo.version) throw new Error("verification failed"); return { ok: true } as const; ``` How it is checked Checked by CI gates Population Every function, build and test run whose result the verification claims to hold Freshness A verdict stands for the code, inputs and dependency versions it ran against, and goes stale when any of them changes Refusal The failing test, proof or analyzer finding fails the gate Observation Test, proof and analyzer results, plus reruns that show whether a result repeats Evidence None, because the catalog states this check as a class, so a watched run belongs to each system that adopts it Authoritative side The specification the test or proof encodes, which a result is compared against Depends on [Specification](https://banes-lab.com/records/lexicon/specification.md), [Correctness](https://banes-lab.com/records/architecture/correctness.md), [Specification Compliance](https://banes-lab.com/records/lexicon/specification-compliance.md) Shape it refuses [Untested Implementation](https://banes-lab.com/records/lexicon/untested-implementation.md) ## Links to - [principle](https://banes-lab.com/records/kind/principle.md) - [recommended](https://banes-lab.com/records/vocabulary/severity-recommended.md) - [Computation Core](https://banes-lab.com/records/layer/computation-core.md) - [Controlled State](https://banes-lab.com/records/lexicon/controlled-state.md) - [Predictability](https://banes-lab.com/records/architecture/predictability.md) - [Reproducibility](https://banes-lab.com/records/architecture/reproducibility.md) - [Reliable Testing](https://banes-lab.com/records/lexicon/reliable-testing.md) - [Runtime Adaptivity](https://banes-lab.com/records/lexicon/runtime-adaptivity.md) - [Hidden Time/Randomness/Global State](https://banes-lab.com/records/lexicon/hidden-time-randomness-global-state.md) - [Referential Transparency](https://banes-lab.com/records/architecture/referential-transparency.md) - [Pure Functions](https://banes-lab.com/records/architecture/pure-functions.md) - [Artificial Intelligence Architecture](https://banes-lab.com/records/architecture/artificial-intelligence-architecture.md) - [Agentic Architecture](https://banes-lab.com/records/architecture/agentic-architecture.md) - [Write Scope and Read Population](https://banes-lab.com/records/architecture/write-scope-and-read-population.md) - [One-Sided Liveness](https://banes-lab.com/records/architecture/one-sided-liveness.md) - [Declare-Before-Read Order](https://banes-lab.com/records/architecture/declare-before-read-order.md) - [Derived Party Count](https://banes-lab.com/records/architecture/derived-party-count.md) - [Externally Resolved Slot](https://banes-lab.com/records/architecture/externally-resolved-slot.md) - [Computation Core](https://banes-lab.com/records/algorithms/computation-core.md) - [Determinism / Runtime Adaptivity](https://banes-lab.com/records/tension/determinism-runtime-adaptivity.md) - [quality-attribute](https://banes-lab.com/records/kind/quality-attribute.md) - [Determinism](https://banes-lab.com/records/architecture/determinism.md) - [Explicit Contracts](https://banes-lab.com/records/architecture/explicit-contracts.md) - [Principle of Least Surprise](https://banes-lab.com/records/architecture/principle-of-least-surprise.md) - [Safe Refactoring](https://banes-lab.com/records/lexicon/safe-refactoring.md) - [Dynamic Runtime Behavior](https://banes-lab.com/records/lexicon/dynamic-runtime-behavior.md) - [Hidden Behavior](https://banes-lab.com/records/lexicon/hidden-behavior.md) - [Runtime Discovery](https://banes-lab.com/records/architecture/runtime-discovery.md) - [Dynamic Binding](https://banes-lab.com/records/architecture/dynamic-binding.md) - [Runtime Extensibility](https://banes-lab.com/records/architecture/runtime-extensibility.md) - [Design by Contract](https://banes-lab.com/records/architecture/design-by-contract.md) - [API Contract](https://banes-lab.com/records/architecture/api-contract.md) - [Postconditions](https://banes-lab.com/records/architecture/postconditions.md) - [Immutability](https://banes-lab.com/records/architecture/immutability.md) - [Repeatability](https://banes-lab.com/records/architecture/repeatability.md) - [Pattern Consistency](https://banes-lab.com/records/architecture/pattern-consistency.md) - [Declarative Configuration](https://banes-lab.com/records/architecture/declarative-configuration.md) - [Convention over Configuration](https://banes-lab.com/records/architecture/convention-over-configuration.md) - [State Isolation](https://banes-lab.com/records/architecture/state-isolation.md) - [Controlled Side Effects](https://banes-lab.com/records/architecture/controlled-side-effects.md) - [Predictability / Dynamic Runtime Behavior](https://banes-lab.com/records/tension/dynamic-runtime-behavior-predictability.md) - [Correctness](https://banes-lab.com/records/architecture/correctness.md) - [Interoperability](https://banes-lab.com/records/architecture/interoperability.md) - [Testability](https://banes-lab.com/records/architecture/testability.md) - [Concurrency Correctness](https://banes-lab.com/records/lexicon/concurrency-correctness.md) - [Maintainability](https://banes-lab.com/records/lexicon/maintainability.md) - [Security](https://banes-lab.com/records/lexicon/security.md) - [Startup Cost](https://banes-lab.com/records/lexicon/startup-cost.md) - [Static Safety](https://banes-lab.com/records/lexicon/static-safety.md) - [Thread Safety](https://banes-lab.com/records/lexicon/thread-safety.md) - [Tests](https://banes-lab.com/records/lexicon/tests.md) - [Contracts](https://banes-lab.com/records/lexicon/contracts.md) - [contextual](https://banes-lab.com/records/vocabulary/severity-contextual.md) - [Safe Substitution](https://banes-lab.com/records/lexicon/safe-substitution.md) - [Stateful IO](https://banes-lab.com/records/lexicon/stateful-io.md) - [Side Effects](https://banes-lab.com/records/lexicon/side-effects.md) - [Referential Transparency / Stateful IO](https://banes-lab.com/records/tension/referential-transparency-stateful-io.md) - [Code Review](https://banes-lab.com/records/architecture/code-review.md) - [technique](https://banes-lab.com/records/kind/technique.md) - [No Side Effects](https://banes-lab.com/records/lexicon/no-side-effects.md) - [Explicit Inputs](https://banes-lab.com/records/lexicon/explicit-inputs.md) - [Stateful Operations](https://banes-lab.com/records/lexicon/stateful-operations.md) - [Hidden IO](https://banes-lab.com/records/lexicon/hidden-io.md) - [Pure Functions / Stateful Operations](https://banes-lab.com/records/tension/pure-functions-stateful-operations.md) - [Value Semantics](https://banes-lab.com/records/lexicon/value-semantics.md) - [Safe Sharing](https://banes-lab.com/records/lexicon/safe-sharing.md) - [Allocation Cost](https://banes-lab.com/records/lexicon/allocation-cost.md) - [Shared Mutable State](https://banes-lab.com/records/architecture/shared-mutable-state.md) - [Value Object](https://banes-lab.com/records/architecture/value-object.md) - [Independent Lifetime Axes](https://banes-lab.com/records/architecture/independent-lifetime-axes.md) - [Immutability / Allocation Cost](https://banes-lab.com/records/tension/allocation-cost-immutability.md) - [Versioned Inputs](https://banes-lab.com/records/lexicon/versioned-inputs.md) - [Auditability](https://banes-lab.com/records/architecture/auditability.md) - [Debugging](https://banes-lab.com/records/lexicon/debugging.md) - [Compliance](https://banes-lab.com/records/architecture/compliance.md) - [Continuous Updates](https://banes-lab.com/records/lexicon/continuous-updates.md) - [Floating Dependencies](https://banes-lab.com/records/lexicon/floating-dependencies.md) - [Flaky Test Normalization](https://banes-lab.com/records/architecture/flaky-test-normalization.md) - [Environment Parity](https://banes-lab.com/records/architecture/environment-parity.md) - [Infrastructure as Code](https://banes-lab.com/records/architecture/infrastructure-as-code.md) - [Immutable Infrastructure](https://banes-lab.com/records/architecture/immutable-infrastructure.md) - [Machine Learning Architecture](https://banes-lab.com/records/architecture/machine-learning-architecture.md) - [Prompt Engineering](https://banes-lab.com/records/architecture/prompt-engineering.md) - [Benchmarking](https://banes-lab.com/records/architecture/benchmarking.md) - [Reproducibility / Continuous Updates](https://banes-lab.com/records/tension/continuous-updates-reproducibility.md) - [mandatory](https://banes-lab.com/records/vocabulary/severity-mandatory.md) - [Verification](https://banes-lab.com/records/architecture/verification.md) - [Reliable Automation](https://banes-lab.com/records/lexicon/reliable-automation.md) - [Real-World Variability](https://banes-lab.com/records/lexicon/real-world-variability.md) - [Environment-Sensitive Behavior](https://banes-lab.com/records/lexicon/environment-sensitive-behavior.md) - [Repeatability / Real-World Variability](https://banes-lab.com/records/tension/real-world-variability-repeatability.md) - [Specification](https://banes-lab.com/records/lexicon/specification.md) - [Validation](https://banes-lab.com/records/architecture/validation.md) - [Safe Operation](https://banes-lab.com/records/lexicon/safe-operation.md) - [Delivery Speed](https://banes-lab.com/records/lexicon/delivery-speed.md) - [Undefined Behavior](https://banes-lab.com/records/lexicon/undefined-behavior.md) - [Domain Model](https://banes-lab.com/records/architecture/domain-model.md) - [Happens-Before Relationship](https://banes-lab.com/records/architecture/happens-before-relationship.md) - [Semantic Contracts](https://banes-lab.com/records/architecture/semantic-contracts.md) - [Preconditions](https://banes-lab.com/records/architecture/preconditions.md) - [Invariant](https://banes-lab.com/records/architecture/invariant.md) - [Formal Verification](https://banes-lab.com/records/architecture/formal-verification.md) - [Specification-Based Testing](https://banes-lab.com/records/architecture/specification-based-testing.md) - [Property-Based Testing](https://banes-lab.com/records/architecture/property-based-testing.md) - [Fail Fast](https://banes-lab.com/records/architecture/fail-fast.md) - [Error Handling](https://banes-lab.com/records/architecture/error-handling.md) - [Design Review](https://banes-lab.com/records/architecture/design-review.md) - [First-Principles Design](https://banes-lab.com/records/architecture/first-principles-design.md) - [Model Evaluation](https://banes-lab.com/records/architecture/model-evaluation.md) - [Finite State Machine](https://banes-lab.com/records/architecture/finite-state-machine.md) - [Schema Validation](https://banes-lab.com/records/architecture/schema-validation.md) - [Type Safety](https://banes-lab.com/records/architecture/type-safety.md) - [Single Source of Truth](https://banes-lab.com/records/architecture/single-source-of-truth.md) - [Semantic Consistency](https://banes-lab.com/records/architecture/semantic-consistency.md) - [Input Validation](https://banes-lab.com/records/architecture/input-validation.md) - [Atomicity](https://banes-lab.com/records/architecture/atomicity.md) - [ACID](https://banes-lab.com/records/architecture/acid.md) - [Consistency](https://banes-lab.com/records/architecture/consistency.md) - [Isolation](https://banes-lab.com/records/architecture/isolation.md) - [Concurrency Control](https://banes-lab.com/records/architecture/concurrency-control.md) - [Correctness / Delivery Speed](https://banes-lab.com/records/tension/correctness-delivery-speed.md) - [Observability](https://banes-lab.com/records/architecture/observability.md) - [Robustness](https://banes-lab.com/records/lexicon/robustness.md) - [Simplicity](https://banes-lab.com/records/lexicon/simplicity.md) - [Model Safety](https://banes-lab.com/records/architecture/model-safety.md) - [Resilience](https://banes-lab.com/records/architecture/resilience.md) - [activity](https://banes-lab.com/records/kind/activity.md) - [Formal Specification](https://banes-lab.com/records/lexicon/formal-specification.md) - [Mathematical Assurance](https://banes-lab.com/records/lexicon/mathematical-assurance.md) - [Cost/Complexity](https://banes-lab.com/records/lexicon/cost-complexity.md) - [Informal Validation Only](https://banes-lab.com/records/lexicon/informal-validation-only.md) - [Formal Verification / Cost/Complexity](https://banes-lab.com/records/tension/cost-complexity-formal-verification.md) - [Behavior Validation](https://banes-lab.com/records/lexicon/behavior-validation.md) - [Spec Maintenance](https://banes-lab.com/records/lexicon/spec-maintenance.md) - [Implementation-Only Testing](https://banes-lab.com/records/lexicon/implementation-only-testing.md) - [Mock Mirage](https://banes-lab.com/records/architecture/mock-mirage.md) - [Test Coverage Kernel](https://banes-lab.com/records/algorithms/test-coverage-kernel.md) - [Specification-Based Testing / Spec Maintenance](https://banes-lab.com/records/tension/spec-maintenance-specification-based-testing.md) - [Properties/Invariants](https://banes-lab.com/records/lexicon/properties-invariants.md) - [Broad Input Exploration](https://banes-lab.com/records/lexicon/broad-input-exploration.md) - [Shrinking/Debug Complexity](https://banes-lab.com/records/lexicon/shrinking-debug-complexity.md) - [Example-Only Testing](https://banes-lab.com/records/lexicon/example-only-testing.md) - [Property-Based Testing / Shrinking/Debug Complexity](https://banes-lab.com/records/tension/property-based-testing-shrinking-debug-complexity.md) - [mechanism](https://banes-lab.com/records/kind/mechanism.md) - [Ruleset](https://banes-lab.com/records/lexicon/ruleset.md) - [Architecture Compliance](https://banes-lab.com/records/lexicon/architecture-compliance.md) - [Automated Enforcement](https://banes-lab.com/records/lexicon/automated-enforcement.md) - [False Positives](https://banes-lab.com/records/lexicon/false-positives.md) - [Unchecked Dynamic Code](https://banes-lab.com/records/lexicon/unchecked-dynamic-code.md) - [Metaprogramming](https://banes-lab.com/records/architecture/metaprogramming.md) - [Reflection](https://banes-lab.com/records/architecture/reflection.md) - [Plugin Architecture](https://banes-lab.com/records/architecture/plugin-architecture.md) - [Static Analysis / False Positives](https://banes-lab.com/records/tension/false-positives-static-analysis.md) - [Low Coupling](https://banes-lab.com/records/architecture/low-coupling.md) - [Deterministic Behavior](https://banes-lab.com/records/lexicon/deterministic-behavior.md) - [Dependency Inversion Principle](https://banes-lab.com/records/architecture/dependency-inversion.md) - [Regression Safety](https://banes-lab.com/records/lexicon/regression-safety.md) - [Encapsulation Extremes](https://banes-lab.com/records/lexicon/encapsulation-extremes.md) - [Hidden Dependencies](https://banes-lab.com/records/lexicon/hidden-dependencies.md) - [Test Pyramid Inversion](https://banes-lab.com/records/architecture/test-pyramid-inversion.md) - [Interface-Based Design](https://banes-lab.com/records/architecture/interface-based-design.md) - [Single Responsibility Principle](https://banes-lab.com/records/architecture/single-responsibility.md) - [High Cohesion](https://banes-lab.com/records/architecture/high-cohesion.md) - [Singleton Pattern](https://banes-lab.com/records/architecture/singleton-pattern.md) - [Stateless Processing](https://banes-lab.com/records/architecture/stateless-processing.md) - [Dependency Injection](https://banes-lab.com/records/architecture/dependency-injection.md) - [Service Locator Pattern](https://banes-lab.com/records/architecture/service-locator-pattern.md) - [Ports and Adapters Architecture](https://banes-lab.com/records/architecture/ports-and-adapters-architecture.md) - [Hexagonal Architecture](https://banes-lab.com/records/architecture/hexagonal-architecture.md) - [Clean Architecture](https://banes-lab.com/records/architecture/clean-architecture.md) - [Testability / Encapsulation Extremes](https://banes-lab.com/records/tension/encapsulation-extremes-testability.md) - [Explicit Dependencies](https://banes-lab.com/records/lexicon/explicit-dependencies.md) - [Global State](https://banes-lab.com/records/lexicon/global-state.md) - [Architecture Review](https://banes-lab.com/records/architecture/architecture-review.md) - [Acceptance Criteria](https://banes-lab.com/records/lexicon/acceptance-criteria.md) - [Fitness for Use](https://banes-lab.com/records/lexicon/fitness-for-use.md) - [Iteration Speed](https://banes-lab.com/records/lexicon/iteration-speed.md) - [Assumption-Driven Delivery](https://banes-lab.com/records/lexicon/assumption-driven-delivery.md) - [Self-Describing Structures](https://banes-lab.com/records/architecture/self-describing-structures.md) - [Metadata-Driven Design](https://banes-lab.com/records/architecture/metadata-driven-design.md) - [Canonicalization](https://banes-lab.com/records/architecture/canonicalization.md) - [Validation / Iteration Speed](https://banes-lab.com/records/tension/iteration-speed-validation.md) - [Specification Compliance](https://banes-lab.com/records/lexicon/specification-compliance.md) - [Cost](https://banes-lab.com/records/lexicon/cost.md) - [Untested Implementation](https://banes-lab.com/records/lexicon/untested-implementation.md) - [Codebase Verification Kernel](https://banes-lab.com/records/algorithms/codebase-verification-kernel.md) - [Verification / Cost](https://banes-lab.com/records/tension/cost-verification.md) ## Linked from - [The layer topology](https://banes-lab.com/ontology/schema/the-layer-topology.md) - [The membership](https://banes-lab.com/ontology/schema/the-membership.md)