Guides

Articles on the topics

Each page explains one idea in general: what a specification claims, what a loop invariant is, and what a passing check does not establish. You can read them on their own.

• What is formal verification?A precise claim about every allowed behavior, checked against a specification instead of a few tests.9 min
• Loop invariantsA fact that stays true at the top of a loop, and becomes the postcondition when the loop stops.9 min