Movy

movy

Movy is a Move testing framework that offers:

Modular low-level building bricks for Move language. Specifically, the executor and tracer abstractions and layered database design borrowed from revm that allow you to emulate and inspect an execution.
Static analysis capabilities inherited from MoveScan, the state-of-the-art static analyzer.
Cutting-edge fuzzing reimplemented from scratch learned from Belobog that supports both property testing and on-chain fuzzing, in the a flavor similar to foundry by writing invariants in Move language.
And a lot of more…

This book serves as documents and tutorials for Movy.

Please note that Movy is at pre-alpha stage, which typically means it could contain bugs. However, rest assured that Movy never makes any real transactions to the live chain and thus your assets and private keys will always remain safe.

Citation

Consider citing our works:

@misc{belobog,
      title={Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts}, 
      author={Wanxu Xia and Ziqiao Kong and Zhengwei Li and Yi Lu and Pan Li and Liqun Yang and Yang Liu and Xiapu Luo and Shaohua Li},
      year={2025},
      eprint={2512.02918},
      archivePrefix={arXiv},
      primaryClass={cs.CR},
      url={https://arxiv.org/abs/2512.02918}, 
}

@inproceedings{movescan,
    author = {Song, Shuwei and Chen, Jiachi and Chen, Ting and Luo, Xiapu and Li, Teng and Yang, Wenwu and Wang, Leqing and Zhang, Weijie and Luo, Feng and He, Zheyuan and Lu, Yi and Li, Pan},
    title = {Empirical Study of Move Smart Contract Security: Introducing MoveScan for Enhanced Analysis},
    year = {2024},
    isbn = {9798400706127},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    url = {https://doi.org/10.1145/3650212.3680391},
    doi = {10.1145/3650212.3680391},
    abstract = {Move, a programming language for smart contracts, stands out for its focus on security. However, the practical security efficacy of Move contracts remains an open question. This work conducts the first comprehensive empirical study on the security of Move contracts. Our initial step involves collaborating with a security company to manually audit 652 contracts from 92 Move projects. This process reveals eight types of defects, with half previously unreported. These defects present potential security risks, cause functional flaws, mislead users, or waste computational resources. To further evaluate the prevalence of these defects in real-world Move contracts, we present MoveScan, an automated analysis framework that translates bytecode into an intermediate representation (IR), extracts essential meta-information, and detects all eight defect types. By leveraging MoveScan, we uncover 97,028 defects across all 37,302 deployed contracts in the Aptos and Sui blockchains, indicating a high prevalence of defects. Experimental results demonstrate that the precision of MoveScan reaches 98.85\%, with an average project analysis time of merely 5.45 milliseconds. This surpasses previous state-of-the-art tools MoveLint, which exhibits an accuracy of 87.50\% with an average project analysis time of 71.72 milliseconds, and Move Prover, which has a recall rate of 6.02\% and requires manual intervention. Our research also yields new observations and insights that aid in developing more secure Move contracts.},
    booktitle = {Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis},
    pages = {1682–1694},
    numpages = {13},
    keywords = {Defect, Move language, Program analysis, Smart contract},
    location = {Vienna, Austria},
    series = {ISSTA 2024}
    }

Installation

Depending on your usage, you could use movy in several ways.

Use Movy as a Tool

It is the most common usage and we recommend using Movy via docker.

docker run --rm movyrs/movy --help

This shall print the help menu of Movy.

Additionally, you could also build Movy locally.

# Install dependencies on Ubuntu/Debian
apt install -y libssl-dev libclang-dev libz3-dev
# Install dependencies on macOS
brew install z3

# Build movy
git clone https://github.com/BitsLabSec/movy
cd movy && cargo build --release

This takes several minutes even on a powerful machine.

Use Movy as a Library

Add this to your Cargo.toml

movy = {git = "https://github.com/BitsLabSec/movy", branch = "master"}

A Tour of Invariant Testing

This chapter will cover the invariant testing step by step.

Please ensure you have installed Movy following our instructions.

The code sample could be found at here. We will use the Sui flavor in this tutorial.

Code Under Testing

Assume a small code snippet that maintains a counter:

module counter::counter;

public struct Counter has key {
    id: UID,
    value: u64
}

public fun create(ctx: &mut TxContext) {
    let counter = Counter {
        id: object::new(ctx),
        value: 1
    };
    transfer::share_object(counter);
}

public fun increment(counter: &mut Counter, n: u64) {
    counter.value = counter.value + n;
}

public fun value(counter: &Counter): u64 {
    counter.value
}

In general, every object shared by this modules contains a u64 value. It is obvious that the value is always positive and now we would like to verify this via Movy.

Add Movy

First, we add the following lines to the Move.toml.

[dev-dependencies]
movy = {git = "https://github.com/BitsLabSec/movy", subdir = "move/movy", rev = "master"}

This allows your code to interact with Movy.

Note the Movy dependency is added to dev-dependencies, i.e. the Movy code will never really go live and does not affect the integrity of the existing modules.

The very first step is deploying the target packages. In the counter example above, Movy need at least one Counter object so that we could test the functions. To create shared objects (and possibly do other setup), add these lines in tests/movy.move with the target package.

Note the Movy modules are organized as unit tests and will only exist in the local emulated environment. It is worth mentioning that Sui rejects any testing modules or testing functions.

#[test_only]
module counter::counter_tests;

use sui::test_scenario::{Self as ts};
use counter::counter::{Self, Counter};
use sui::bag::Self;

#[test]
public fun movy_init(
    deployer: address,
    attacker: address
) {
    let mut scenario = ts::begin(deployer);
    {
        ts::next_tx(&mut scenario, deployer);
        counter::create(ts::ctx(&mut scenario));
    };

    ts::next_tx(&mut scenario, attacker);
    {
        let mut counter_val = ts::take_shared<Counter>(&scenario);
        counter::increment(&mut counter_val, 0);
        ts::return_shared(counter_val);
    };

    ts::end(scenario);
}

We will break down the code snippet:

#[test_only] ensures that the module itself will never be used in a production environment and enables test_scenario, which further allows us to do multi transaction deployment.
movy_init is a special function in Movy that will be called after the module is deployed. The deployer will be the one that deployed the target module, in this case, the counter module while the attacker will be the one trying to attack the module. In general, a movy_init should always transfer administration capabilities to deployer while grants minimal permission to attacker for a real-world scenario.
ts::begin, ts::next_tx and ts::end starts a multi-transaction testing scenario.
ts::take_shared and ts::return_shared create a shared object and use it immediately with increment, which will only works in a testing module with testing_scenario. This essentially simulates two transactions of the deployment because shared objects are not possible to create and use within a single transaction.

Movy will call movy_init during fuzzing and movy_init is supposed to setup the target modules. All changes will be captures and the shared objects created will be used in the following fuzzing campaign.

If nothing special is needed, movy_init could be omitted or empty.

Write First Movy Test

A Movy test has some special setup compared to ordinary Move tests. The following code presents a minimal Movy test in file tests/movy.move.

use movy::oracle::crash_because;

#[test]
fun extract_counter(ctr: &Counter): (ID, u64) {
    let val = counter::value(ctr);
    let ctr_id = sui::object::id(ctr);
    (ctr_id, val)
}

#[test]
public fun movy_pre_increment(
    movy: &mut context::MovyContext,
    ctr: &mut Counter,
    _n: u64
) {
    let (ctr_id, val) = extract_counter(ctr);
    let state = context::borrow_mut_state(movy);
    bag::add(state, ctr_id, val);
}

#[test]
public fun movy_post_increment(
    movy: &mut context::MovyContext,
    ctr: &mut Counter,
    n: u64
) {
    let (ctr_id, new_val) = extract_counter(ctr);
    let state = context::borrow_state(movy);
    let previous_val = bag::borrow<ID, u64>(state, ctr_id);
    if (*previous_val + n != new_val) {
        crash_because(b"Increment does not correctly inreases internal value.".to_string());
    }
}

Again, we can break down the code:

movy_pre_increment and movy_post_increment are special functions that tell Movy to call them before and after increment function. In other words, if Movy initiates a call to counter::increment, it will inserts the two functions calls to make the transaction sequence like [movy_pre_increment, counter::increment, movy_post_increment]. Movy identifies such functions with a pattern like movy_pre_* and movy_post_*.
context::MovyContext is a fresh wrapper of sui::bag::Bag that allows users to store any context. In this case, we store the value before increment. It should be always the first argument of the movy_pre_ and movy_post_ functions.
ctr: &mut Counter, n: u64 is the original signature of the counter::increment.
movy::oracle::crash_because will inform Movy that an invariant violation happens and Movy will capture the seed as a crash.
The core logic of the invariant is that, before the counter::increment call, we store the value in movy_pre_increment. After the counter::increment call, we get the value and check if the value exactly increases by n. If not, movy::oracle::crash_because will tell Movy to save this seed.

Run Movy

Finally, it is time to test the invariants we just wrote:

RUST_LOG=info ./target/release/movy sui fuzz
    -l ./test-data/counter
    -o /tmp/out

RUST_LOG=info will print some helpful logs.
-l ./test-data/counter points to the target package with the Movy test modules.
-o /tmp/out will tell Movy to save outputs to /tmp/out and we will cover this later.

You could see logs like:

[INFO  movy_replay::env] Committing testing std 0x000000000000000000000000000000000000000000000000000000000000000b
[INFO  movy_replay::env] Committing testing std 0x0000000000000000000000000000000000000000000000000000000000000001
[INFO  movy_replay::env] Committing testing std 0x0000000000000000000000000000000000000000000000000000000000000002
[INFO  movy_replay::env] Committing testing std 0x0000000000000000000000000000000000000000000000000000000000000003
...
[INFO  movy::sui::env] Deploying the local package at ./test-data/counter/
[INFO  movy_replay::env] Compiling ./test-data/counter/ with test mode...
[INFO  movy_replay::env] Detected a movy_init at: 0x9ae10865d456c2a9ebc47b754db3f77b96eebb049192a26fce0577aaca3a5e2a::counter_tests
[INFO  movy_replay::env] Commiting movy_init effects...
...
[INFO  movy_fuzz::operations::sui_fuzz] [Client Heartbeat #0] run time: 33s, clients: 1, corpus: 3, objectives: 0, executions: 326, exec/sec: 9.632, code-fb: 68/16384 (0%), stability: 1/1 (100%)

Generally, Movy does the following things to test the contracts.

First, Movy will spin up an empty fork of the Chain, in this case, the Sui chain.
Movy will deploy the Sui standard framework to the fork in the testing mode, which enables the 0x1::unit_test and 0x2::test_scenario.
Then Movy will invoke the Move compiler to compile the given project ./test-data/counter to obtain modules and their interfaces.
Movy further will deploy the modules to our fork (at 0x9ae10865d456c2a9ebc47b754db3f77b96eebb049192a26fce0577aaca3a5e2a) and execute movy_init in the testing modules.
Once everything is ready, Movy starts to assemble random transactions. Gnerally, the corpus metrics indicates the number of interesting inputs, the objectives indicates the number of crashing inputs that violate invariants and code-fb refers to the code coverage.

Trigger a Violation

The fuzzing in the previous section shall work, but not really trigger a crash because the invariant always holds. Now let’s manually add a bug for our counter implementation:

public fun increment(counter: &mut Counter, n: u64) {
-    counter.value = counter.value + n;
+    counter.value = counter.value + 1;
}

Note we intentionally broke the invariant: only increase 1 though users request to increas n. Rerun Movy with the project and we could see:

...
[INFO  movy_fuzz::operations::sui_fuzz] [Objective #0] run time: 24s, clients: 1, corpus: 2, objectives: 3, executions: 247, exec/sec: 10.27, code-fb: 104/16384 (0%), stability: 1/1 (100%), crash-fb: 118/16384 (0%)

In case you see errors like “The given output is already there….”, rerun Movy with -f parameter to automatically remove the existing results. The mechanism is to prevent accidental removal of previous fuzzing campaigns.

Movy immediately could find a objectives and this indicates that we found the violations.

Replay and Inspect a Violation

In addition to finding violations, Movy also supports inspect how violation happens by replaying the violations. Recall that we have the -o /tmp/out option to Movy to save outputs to /tmp/out and it is time to see the contents.

> ls /tmp/out
args.json  crashes/  env.bin  fuzz_meta.json  queue/

args.json is the arguments that start Movy, i.e., the CLI parameters.
fuzz_meta.json is the metadata we setup for the fuzzing campaign, including the target contracts and their interfaces.
env.bin is a binary file that holds our forked chain contents.
queue/ saves the interesting seeds and we can ignore it in this tutorial.
crashes/ saves the violations Movy have found.

Since we have found some violations, we shall have at least crashes/0.json and we can replay it by providing the saved environment:

RUST_LOG=info ./target/release/movy sui replay-seed \
        -s /tmp/out/crashes/0.json \
        -e /tmp/out/env.bin \
        -m /tmp/out/fuzz_meta.json \
        --trace

The output of a full trace is usually very long. Saving to a text file and using an editor is highly recommended.

This will print a full trace including everything during execution and we could see that:

├─ 0x977654ad5e98ce5a09b7bbac3421b312aef7370b0bfc889e6181a8bcc23d8b9c:counter_tests:movy_post_increment(...)
...
│  └─ 0x977654ad5e98ce5a09b7bbac3421b312aef7370b0bfc889e6181a8bcc23d8b9c:oracle:crash_because(...)

So the invariant violation happens exactly in movy_post_increment.

Movy Book