Verification in the Wild
onerous bugs, there is a steep learning
curve and a large time investment.
Model checking. Another formal
method—model checking—can also
determine if a system is provably cor-
rect. Model checkers use state-space
exploration systematically to enumer-
ate paths for a system. Once all paths
have been executed, a system can be
said to be correct. Examples of model
checkers include Spin, 11 MoDIST, 14
TLC, 7 and MaceMC. 6
Given the multitude of inputs and
failure modes a system can experience,
however, running an exhaustive model
checker is incredibly time and resource
Composite. Some of the objections
to and costs of formal verification
methods could be overcome if provably
correct components composed with
one another to create provably correct
systems. However, this is not the case.
Often components are verified under
different failure models, and these ob-
viously do not compose. In addition,
the correctness specifications for each
component do not compose together
to create a correctness specification
for the resulting system. 1 To prove the
resulting system is provably correct, a
new correctness specification must be
created and the tests must be rerun.
Creating a new correctness specifi-
cation for each combination of compo-
nents does not scale well, especially in
the microservice-oriented architectures
that have recently become popular.
Such architectures consist of anywhere
from tens to thousands of distinct ser-
vices, and writing correctness specifica-
tions at this scale is not tenable.
Given that formal verification is expensive and does not produce components
that can be composed into provably correct systems without additional work,
one may despair and claim the problem
seems hopeless, distributed systems are
awful, and we cannot have nice things.