The Move Prover: Quality Assurance of Formal Verification

This report describes a verification pitfall encountered when using the Move Prover on an Aptos Move module: an overly-abstracted specification for coin_address led the prover to conclude a function unconditionally aborts, allowing incorrect postconditions to be proved. The authors diagnosed the issue using --check-inconsistency and --unconditional-abort-as-inconsistency flags, reported and fixed the specification in Aptos, and recommend QA steps and careful review of surrounding specifications when performing formal verification.