Not every problem is a proof problem, and saying so is part of the method. This topic covers three applications that surround the core: a non-interference check that catches value leaks but not timing channels, a dead-state analysis where an unreached cover is inconclusive until an invariant proves it, and the precise boundary with the CDC, low-power and CPU flows, where formal checks the protocol around an abstraction and the owner flow checks the rest. Each lesson states what its proof does not show.
Lesson | After it you can... |
|---|---|
Prove a secret stays hidden while locked, including after a re-lock, and state the timing-channel limit. | |
Prove a state unreachable instead of merely uncovered, and check a case statement for latches. | |
Hand each neighbour flow its checking job with the right link. |
Suggested order: top to bottom. The security invariant first, because the two-copy harness is already familiar; dead states next, because the cover-versus-proof distinction pays off everywhere; the boundary lesson last, because it tells you when to stop proving and start linking.
When another flow owns the mechanism: synchroniser design, power intent, pipeline micro-architecture. Formal contributes one check at the boundary, and the lesson links out for the rest.