# Formal Verification

> The activity of proving, against a formal specification, that an algorithm or protocol keeps its invariants for every input.

Record: `architecture:formal-verification`
Kind: activity
Layer: [Computation Core](https://banes-lab.com/records/layer/computation-core.md)
Severity: contextual
Scope: algorithm, protocol, critical system
Canonical: https://banes-lab.com/ontology#architecture-formal-verification

Listed in [Architecture principles](https://banes-lab.com/api/records/architecture.md), after [Correctness](https://banes-lab.com/records/architecture/correctness.md) and before [Specification-Based Testing](https://banes-lab.com/records/architecture/specification-based-testing.md).

## Repair

- Refactored by: Specify Model, Prove Invariant
- Detected by: missing formal model for critical invariant
- Violated by: critical logic without proof where required
- Measured by: proven property coverage
- Enforced by: proof tooling

## 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)

## Conflicts with

- [Informal Validation Only](https://banes-lab.com/records/lexicon/informal-validation-only.md)

## In tension with

- [Cost/Complexity](https://banes-lab.com/records/lexicon/cost-complexity.md)

## Tensions

- [Formal Verification / Cost/Complexity](https://banes-lab.com/records/tension/cost-complexity-formal-verification.md)

## Severity

- [contextual](https://banes-lab.com/records/vocabulary/severity-contextual.md)

## Category

- [Correctness / Determinism / Verification](https://banes-lab.com/records/architecture-category/correctness-determinism-verification.md)

## Linked from

- [Scale follows determinism](https://banes-lab.com/software-architecture/scale/scale-follows-determinism.md)
- [Correctness / Determinism / Verification](https://banes-lab.com/ontology/principles/architecture-category-correctness-determinism-verification.md)
- [Correctness / Determinism / Verification](https://banes-lab.com/ontology/lexicon/lexicon-category-correctness-determinism-verification.md)
- [Severity levels](https://banes-lab.com/ontology/schema/the-vocabulary-severity.md)
- [The resolutions](https://banes-lab.com/ontology/schema/the-resolutions.md)