Move Mutation Testing

Overview

Equilibrium built mutation-testing tooling for the Move language, for the Aptos ecosystem (with support from the Aptos Foundation, and co-published with Aptos Labs). Mutation testing introduces small, deliberate changes (“mutants”) into source code and checks whether the existing tests and formal specifications still catch them. This is a direct measure of how good those tests and specs are.

The assurance from Aptos’s Move Prover (its formal-verification tool) is only as strong as the user-written specifications: weak or incomplete specs can give a false sense of security. This tooling surfaces those blind spots.

Deliverables

• move-mutator: mutates Move source code (generating mutants), leaving tests and spec blocks untouched.
• move-spec-test: applies mutation testing to evaluate the completeness of Move Prover specifications: runs mutants against the unchanged specs via the Move Prover to see whether the specs detect them.
• move-mutation-test: measures test-suite quality, checks whether the original test suite “kills” each mutant.
• Open-sourced at equilibriumco/move-mutation-tools.

Technical highlights

• Brings mutation testing, a well-established software-quality technique, to Move and its formal-specification workflow (the Move Prover).
• Distinguishes two axes of quality: specification completeness (do the Prover specs catch injected faults?) and test-suite quality (do the unit tests?).
• Helps developers eliminate weak spots so formal proofs aren’t undermined by weak specs, improving the formal-verification quality of Move code on Aptos.

Status

Completed and open-sourced (equilibriumco/move-mutation-tools), in collaboration with Aptos. Delivered in 2024.