# Formal Verification

Record: `arch: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#arch-formal-verification

## 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/lex/formal-specification.md)

## reinforces

- [Correctness](https://banes-lab.com/records/arch/correctness.md)

## enables

- [Mathematical Assurance](https://banes-lab.com/records/lex/mathematical-assurance.md)

## conflicts-with

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

## tensions-with

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

## tensions

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