Formal Verification, the Move Language, and the Move Prover

### Executive summary This blog-length primer describes the Move language and its design choices that facilitate formal verification, and demonstrates how to use the Move Prover and the Move specification language to state and prove properties (pre/postconditions, invariants, module/data-structure invariants) with examples (arithmetic overflow, McCarthy 91, bubble sort), while noting limitations, pitfalls (ghost variables, inconsistencies, limited cross-transaction reasoning), and practical guidance for writing useful specifications.