# Model Checking

> Proves that a property holds across the reachable state space

Record: `reasoning:technique-model-checking`
Kind: technique
Canonical: https://banes-lab.com/ontology/reasoning#reasoning-technique-model-checking

Listed in [Reasoning records](https://banes-lab.com/api/records/reasoning.md), after [Chaos Testing](https://banes-lab.com/records/reasoning/technique-chaos-testing.md) and before [Deterministic Replay](https://banes-lab.com/records/reasoning/technique-deterministic-replay.md).

## Mode

- [explanation](https://banes-lab.com/records/reasoning/mode-explanation.md)

## Surfaces

- [functional-correctness](https://banes-lab.com/records/reasoning/test-surface-functional-correctness.md)
- [protocol-correctness](https://banes-lab.com/records/reasoning/test-surface-protocol-correctness.md)

## Linked from

- [The modes](https://banes-lab.com/ontology/reasoning/the-modes.md)
- [The test surfaces](https://banes-lab.com/ontology/reasoning/the-test-surfaces.md)