Simulation shows the design working on the sequences you wrote. A formal run checks a property against every input sequence the model allows, up to a bound or all the way to a proof, and answers in one of three ways: proven, counterexample, or inconclusive. This topic fixes that vocabulary, shows that every proof is relative to its assumptions, gives one honest measurement of what simulation misses, and ends with a practical split of work between the two methods. It assumes the on-ramp lessons below and starts where they stop: with results you must defend.
Lesson | After it you can... |
|---|---|
Read any formal result as proven, counterexample, or inconclusive, and say what bounded to N does and does not promise. | |
Predict how an assumption changes a result, and spot an assumption that hides a bug. | |
Quantify why a deep corner bug escapes random simulation and falls to a bounded check. | |
Assign each obligation to formal or simulation and size a formal model from its state bits. |
Suggested order: top to bottom. The first lesson fixes the vocabulary every later lesson uses. The second shows why that vocabulary always carries an assumption list. The third motivates the cost with one measured bug. The fourth turns the insight into a work split.
Inconclusive, bounded to 12: no counterexample up to 12 steps. That is a sound result with a stated bound, but not a proof; it becomes signoff-grade only with a bound justification.