A Sui Move security article published on November 13, 2026, at 12:26 p.m. (UTC+8) uses Certora Sui Prover to examine what the language’s type system and verifier can guarantee—and what they cannot.
The article identifies five gaps to test for: bits lost during shifts, signed values stored in unsigned integers, privileged functions without caller checks, unverified object ownership, and older package versions that remain callable. Drawing on vulnerabilities involving Cetus, Aftermath Finance, Typus Finance and Scallop, the author describes Certora rules labeled P1–P4 for these gaps and extends the discussion to protocol invariants labeled P5–P8.
The practical takeaway is to define the properties and assumptions to be checked before relying on formal verification. The article also suggests using test_scenario and Sui Prover to test the identified gaps.