The Hitchhiker's Guide to Move, Vol1

Making the Move: Secure Smart Contracts for Rust Developers

With the pretext to learn a new Smart Contract paradigm and cut through the noise and hype, we embark on the epic quest of reading the required papers, articles and documentation of Move, Sui, and Aptos.

Our goal is to understand the key differences between Rust and Move in the context of Smart Contracts, exploring the Move Programming model, its unique features and its differences from other comparable programming models.

Having that in mind we created a simple end to end raffle system, and improved our expertise based on a well-known paper in the Sui community on different random strategies using the DRAND beacon chain method, and aggregated BLS signatures.

This guide marks the beginning of a series of articles that will explore Move and Sui features focusing on real-world, production ready methodologies, and some quirk experiments. Bridging the gap between academic research and hands-on development.

(TL;DR: We will teach you to Move by example, and.. yes!, we love papers)

‍

Why another Language?

The motivation behind Move

To understand why Move was created, we need to go back to the roots of smart contracts and revisit Nick Szabo’s original definition. Let’s return to the basics:‍

“A smart contract is a computerized transaction protocol that executes the terms of a contract. The general objectives of smart contract design are to satisfy common contractual conditions, minimize exceptions both malicious and accidental, and minimize the need for trusted intermediaries. Related economic goals include lowering fraud loss, arbitration and enforcement costs, and other transaction costs”‍

In the case of the EVM (Ethereum Virtual Machine), achieving these goals—such as reducing fraud loss and improving security—requires careful, strategic system design.

However, the process is prone to errors, especially for new developers. While Vyper offers a more security-focused alternative to Solidity, both languages are domain-specific languages (DSLs) that are deeply coupled with the execution environment and its inherent limitations of a deterministic computation.

This flexibility in the EVM, the lack of clear heuristics, and the execution environment and its system constraints comes with a cost: Security. A poorly designed smart contract leads to reentrancy attacks, access control issues, strategic rogue calls and binary bytecode exploitation. 

The Bitcoin-inspired blockchain data structure model leads to interoperability and scalability challenges and limitations. For this reason Ethereum inherited some of these challenges and tried to solve it by vertical scaling, through L2 blockchains.

‍

The birth of Move:

A new approach to Smart Contracts

Recognizing these challenges, the Libra team at Meta set out to design a new model —one that moves beyond the traditional blockchain architecture of a single canonical chain, fixed block space, and layer-2 solutions to address scalability. 

Instead, they proposed a new blockchain based in Directed Acyclic Graphs (DAGs) and a Byzantine Fault Tolerance consensus model, like the one Barbara Liskov explains here

• A virtual Machine to execute the smart contracts: MoveVM
• A new Programming Language: Move
• A novel and expressive Smart Contract Paradigm ( based on Linear Logic )
• A secure subset of logical rules for formal verification, and
  and memory safety rules implemented on top of Rust

This paradigm shift introduced Move, a language specifically designed to handle digital assets as first-class citizens, ensuring safe ownership, resource management, and formal verification as side effects.

Following the initial development of Libra/Diem, the original team split in two groups, to these foundational ideas:

Aptos team: Focused on an account based model similar to the EVM, but with improvements in performance and safety

Sui team: Takes an Object oriented approach, all assets are first class objects, with clearly defined ownership rules, named abilities, and semantic capabilities.‍

In our case we choose Sui for their novel architecture approach , simplicity, tooling, and of course TVL.

Also, Rather Labs has secured a grant from Arbitrum DAO to build a Move-to-WebAssembly (WASM) compiler for Stylus, Arbitrum’s smart contract platform. This project will enable developers to write secure, Move-based smart contracts and deploy them on Arbitrum, leveraging Stylus’ WASM-based infrastructure for enhanced performance and interoperability. By bridging Move’s safety-focused design with Arbitrum’s scalable ecosystem, this initiative opens new possibilities for developers

‍

Comparison with Rust

Move and Rust share similarities in their approach to safety and resource management. However, they are fundamentally different in their goals and use cases.

‍

The Move Programming Model ( Foundations )

In Move, we think in objects and modules, each smart contract is a module, and contains functions and custom types, structs and enums. Functions can call other functions and use the same type system without an explicit interface, like Solidity for example.

Objects are struct instances, stored by the runtime and persisted globally across transactions, there are different types of objects.

• Single Owner: Objects are owned by a single account, granting exclusive control over the object, it’s implemented using public key cryptography

each owned object is associated with a public key using edwards Ed25519 curves

• Shared State: Objects can be shared with the network, allowing multiple accounts to read and modify the object, they are now owned and associated with them.
  
  
• Immutable State: Objects which can't be mutable and can not change their state

Any owned object can be shared and can’t change and once is shared, it can never be transferred or become an owned object again.

The Move smart contract will be built into a bytecode for the Sui compiler and the code will be verified to publish the modules and the resources in the SUI object store.

A client may submit transactions to perform operations like splitting a coin or executing a static call. The tx are processed by the Move Virtual Machine (VM), which executes the specified operations and reads or mutates the blockchain persisting changes (the effects) in the shared object store or the Owned objects, the access control will be given as a side effect of the abilities and the simplified Rust ownership model.

*The dragon is a reference of the Compilers: Principles, Techniques, and Tools book

The Move Prover 

Move was designed to prioritize robustness and security over flexibility compared to Solidity. It achieves this through built-in quality guarantees, such as the Move Prover—a tool that enables formal specification and automated verification of smart contracts.

The Move Prover is a tool that can validate logical properties offering the user experience of a linter or type checker, but internally a lot of complexity and magic is happening. It leverages formal verification, a rigorous mathematical method for proving the correctness of a system’s behavior and logic.

A developer can create the functional properties using the MSL, Move specification Language, Spec in the diagram

‍

Why does formal verification matter ?

We code specs and process it and compile it into a Prover Object Model into a DSL Boogie language, that will be resolved by a Z3 Analyzer(*), all of this process ensures secure and logically proven code. Like Halmos in the EVM world.

_{(*) Z3 is a research theorem prover language to check the satisfiability of logic of code.}

You can learn more about Move Prover from the original paper, here.

‍

Conclusions

Move is more than a language, it is a paradigm shift. By enforcing resource-oriented programming (no dynamic dispatch, strict ownership rules), it eliminates entire classes of bugs: double-spends, unauthorized transfers, and reentrancy. Its integration of formal verification (via Move Prover and Z3) ensures contracts behave exactly as mathematically specified, unlike EVM’s error-prone trial-by-fire auditing.

 
Next Steps

In the next article, we’ll put theory into practice: building a raffle system on Sui to explore hands-on how Move’s resource model, ownership rules, and safety guarantees differ from Rust. Get ready to see why Move redefines secure smart contracts, one verified line at a time.

“The dragon guards the treasure; the prover guards the code.” 🐉🔒

Let's move!