Formal verification of smart contracts:

Solidity vs. Move

Massimo Bartoletti

University of Cagliari

Silvia Crafa

University of Padova

Enrico Lipparini

University of Cagliari

Tokens and smart contracts

• Tokens: BTC, ETH, NFTs, memecoins, …
• Exchange tokens among untrusted users:
• Direct transfers: Alice : transfer 1:BTC to Bob
• Programmable transfers (“smart contracts”)

​

contract BirthdayGift {

deposit() { … } // anyone can deposit tokens

withdraw(){ … } // Alice withdraws tokens on birthday

}

Tokens and smart contracts

• Tokens: BTC, ETH, NFTs, memecoins, …
• Exchange tokens among untrusted users:
• Direct transfers: Alice : transfer 1:BTC to Bob
• Programmable transfers (“smart contracts”)

​

contract BirthdayGift {

deposit() { … } // anyone can deposit tokens

withdraw(){ … } // Alice withdraws tokens on birthday

}

transfer secured by cryptography

execution

secured by cryptography

Security of programmable token transfers

New problems for Computer Science…

• Contract code is public & immutable
• Huge amounts of $$$ at stake (~3 trillion USD)
• Complexity:
• Programming languages for contracts
• Economic models (“Decentralized Finance”)
• Properties (structural, economic, game-theoretic, …)

Source: https://www.chainalysis.com/blog/crypto-hacking-stolen-funds-2025/

Source: https://www.chainalysis.com/blog/crypto-hacking-stolen-funds-2025/

Research challenges

• Need for formal specs: when is a contract secure?
• Need for formal proofs: is my contract secure?
• Most analysis tools used in practice do not guarantee security…

CONTRACT

ANALYSIS TOOL

integer overflow

improper access control

unhandled exception

…

Majority of losses (~90%) due to logical errors in contracts! doi.org/10.1145/3597503.3623302

❌

✅

✅

Research challenges

• Need for formal specs: when is a contract secure?
• Need for formal proofs: is my contract secure?
• Verification tools can guarantee security

CONTRACT

SPEC

VERIFICATION TOOL

OK

NO

The effectiveness of verification tools largely depends on contract / spec languages

Different blockchain designs, different smart contract languages

Accounting model

UTXO-based

account-based

stateful

stateless

Ethereum

Solana

Tezos

Algorand

Cardano

Bitcoin

Aptos

SUI

Avalanche

Hedera

Different blockchain designs, different smart contract languages

Accounting model

UTXO-based

account-based

stateful

stateless

Ethereum

Solana

Tezos

Algorand

Cardano

Bitcoin

Aptos

SUI

Avalanche

Hedera

Solidity

Move

Resource linearity: Solidity-style

contract Bank {

mapping (address => uint) credits ;

​

function deposit () payable { // receives msg.value ETH from msg.sender

credits[msg.sender] += msg . value ; // adds credits of msg.sender

}

​

function withdraw (uint amount ) {

credits [msg.sender] -= amount; // removes credits of msg.sender

payable (msg.sender ).transfer (amount) ; // sends amount ETH to msg.sender

}

}

Resource linearity: Solidity-style

contract Bank {

mapping (address => uint) credits ;

​

function deposit () payable { // get msg.value ETH from msg.sender

credits[msg.sender] += msg . value ; // add credits of msg.sender

// after 1000 lines of code…

if (unlucky(msg.sender))

credits[msg.sender] = 0;

}

​

function withdraw (uint amount ) {

credits [msg.sender] -= amount; // remove credits of msg.sender

payable (msg.sender ).transfer (amount) ; // send amount ETH to msg.sender

}

}

resources are destroyed!

Resource linearity: Move-style

module bank {

struct Bank { credits : SimpleMap<address, Coin> } // Bank is a resource

​

fun init (owner : &signer) {

let bank = Bank { credits:simple_map::new() }; // create a Bank resource

move_to(owner, bank ) ; // move resource to owner’s account

}

fun deposit (sender : &signer, owner : address, amount : u64) {

… // retrieve Bank resource associated to owner

… // move amount coins from sender’s account to sender’s entry in Bank’s credits

}

fun withdraw(sender : &signer, owner : address, amount : u64 ) { ... }

}

Resource linearity: Move-style

deposit (sender = 0xBB, owner = 0xAA , amount = 2)

let to_deposit = coin::withdraw(sender, amount);

let bank = borrow_global_mut<Bank>(owner);

let credit = map::borrow_mut(&mut bank.credits, address_of(sender) ) ;

coin::merge(credit, to_deposit);

owner (0xAA)

sender (0xBB)

Bank {credits}

Resource linearity: Move-style

deposit (sender = 0xBB, owner = 0xAA , amount = 2)

let to_deposit = coin::withdraw(sender, amount);

let bank = borrow_global_mut<Bank>(owner);

let credit = map::borrow_mut(&mut bank.credits, address_of(sender) ) ;

coin::merge(credit, to_deposit);

​

owner (0xAA)

sender (0xBB)

Bank {credits}

Resource linearity: Move-style

deposit (sender = 0xBB, owner = 0xAA , amount = 2)

let to_deposit = coin::withdraw(sender, amount);

let bank = borrow_global_mut<Bank>(owner);

let credit = map::borrow_mut(&mut bank.credits, address_of(sender) ) ;

coin::merge(credit, to_deposit);

​

owner (0xAA)

sender (0xBB)

Bank {credits}

Resource linearity: Move-style

deposit (sender = 0xBB, owner = 0xAA , amount = 2)

let to_deposit = coin::withdraw(sender, amount);

let bank = borrow_global_mut<Bank>(owner);

let credit = map::borrow_mut(&mut bank.credits, address_of(sender) ) ;

coin::merge(credit, to_deposit);

​

owner (0xAA)

sender (0xBB)

Bank {credits}

Research questions

How do the designs of Solidity and Move affect the effectiveness of program verification?

What types of properties can mainstream verification tools for Solidity and Move check?

Are there important properties that current verification tools cannot even express?

Research questions

How do the designs of Solidity and Move affect the effectiveness of program verification?

What types of properties can mainstream verification tools for Solidity and Move check?

Are there important properties that current verification tools cannot even express?

blockchain-unica / solidity-vs-move-verification

◾Bank

◾Vault

◾Bet

Use cases

◾Bank (28)

◾Vault (22)

◾Bet (17)

Specs

Solidity contracts

(Aptos) Move contracts

CVL specs

MSL specs

Certora Prover

Move Prover

Ground truth + verification outcome + explanation

Solidity vs. Move

Resource linearity

deposit-assets-credit: “after a successful deposit of n tokens, the credits of the sender are increased by n”

deposit-assets-transfer: “after a successful deposit of n tokens, n tokens pass from the control of the sender to that of the contract.”

contract Bank {

mapping (address => uint) private credits;

​

function deposit() payable {

credits[msg.sender] += msg.value;

}

​

...

​

}

module bank {

struct Bank has key, store {

credits: SimpleMap<address, Coin<AptosCoin>>,

}

fun deposit(sender:&signer, owner:address, amount:u64) {

let bank = borrow_global_mut<Bank>(owner);

let to_deposit = coin::withdraw(sender,amount);

let credit = map::borrow_mut(&mut bank.credits,

address_of(sender));

coin::merge(credit, deposit);

}

...

}

Resource linearity

deposit-assets-credit: “after a successful deposit of n tokens, the credits of the sender are increased by n”

deposit-assets-transfer: “after a successful deposit of n tokens, n tokens pass from the control of the sender to that of the contract.”

Access control and ownership

fun f(owner: &signer, receiver: address, amt: uint) {

let addr_sender = signer::address_of(owner);

let s = borrow_global_mut<C<CoinType>>(addr_sender);

coin::deposit<CoinType>(

receiver,� coin::extract(&mut s.coins, amt));

}

function f(address receiver, uint amt) {

require (msg.sender == owner);

receiver.transfer(amt);

}

f-abort: “a call to f() aborts if the sender is not the owner”

Assets transfer (1)

fun f(owner: &signer, receiver: address, amt: uint) {

let addr_sender = signer::address_of(owner);

let s = borrow_global_mut<C<CoinType>>(addr_sender);

coin::deposit<CoinType>(

receiver,� coin::extract(&mut s.coins, amt));

}

function f(address receiver, uint amt) {

require (msg.sender == owner);

receiver.transfer(amt);

}

​

f-not-abort: “a call to f() does not abort if the sender is the owner”

* aborts if receiver is a contract whose receive function fails

Assets transfer (2)

fun f(owner: &signer, receiver: address, amt: uint) {

let addr_sender = signer::address_of(owner);

let s = borrow_global_mut<C<CoinType>>(addr_sender);

coin::deposit<CoinType>(

receiver,� coin::extract(&mut s.coins, amt));

}

function f(address receiver, uint amt) {

require (msg.sender == owner);

(bool succ,) =

receiver.call{value: amt}("");

require(succ);

}

f-assets-transfer: “after a successful call to f(), amt tokens pass from the contract to the receiver”

* low-level call might have enough gas to transfer tokens to another address

Function dispatching

module bet {

fun win(player: &signer, owner: address) {

let bet = borrow_global_mut<Bet<CoinType>>(owner);

assert!(oracle::get_rate(bet.oracle) >= 5);

let value = coin::value(&bet.pot);

let prize = coin::extract(&mut bet.pot, value);

coin::deposit(signer::address_of(player), prize);

} ...

}

contract Oracle {

function get_rate() { return 10; } ...

}

contract Bet {

function win() {

Oracle o = Oracle(oracle);

require(o.get_rate() >= 5);

player.transfer(address(this).balance);

}

}

price-bet/win-revert: “a call to win() aborts if the oracle exchange rate is less than 5”

2: must instruct the verifier to bind o to an Oracle contract

1: sound, because target address o could be anything

Certora vs. Move Prover

Function specs

rule deposit_assets_credit {

env e;

mathint amt = e.msg.value;

mathint snd = e.msg.sender;

mathint old_v = currentContract.credits[snd];

deposit(e);

mathint new_v = currentContract.credits[snd];

assert new_v == old_v + amt;

}

spec bank_addr::bank {

spec deposit {

let snd = signer::address_of(sender);

let old_c = global<Bank>(owner).credits;

let old_v = map::spec_get(old_c,snd).value;

let post new_c = global<Bank>(owner).credits;

let post new_v = map::spec_get(new_c,snd).value;

ensures new_v == old_v + amt;

}

}

deposit-assets-credit: “after a successful deposit of n tokens, the credits of the sender are increased by n”

Properties that specifically target a given function

• Success conditions: characterize when a function aborts or not
• Post-conditions: express properties of the state after the call

State invariants

“for every reachable state s, it holds that P(s)”

where P(s) is a property that only mentions state variables

Two types:

• Inter-function:

reachable states = states that are reachable across function calls�

- Certora: state invariants

- Move Prover: struct invariants or global invariants

​

• Intra-function:

reachable states = states reachable within executions of functions�

- Certora: ghost variables + hooks

- Move Prover: no (in general), yes (for global state updates)

Single-transition invariants

rule assets_dec_onlyif_deposit {

env e; method f; calldataarg args;

...

f(e, args); // f arbitrary function

...

assert new_a_bal < old_a_bal =>

(f.selector == sig:deposit().selector

&& e.msg.sender == a);

}

spec bank_addr::bank {

let addr_sender = signer::address_of(sender);

spec withdraw {

...

ensures sender_coins_value_post >= sender_coins_value;

}

spec deposit {

...

ensures forall a: address where a!=addr_sender :

coin.value >= old(coin.value);

}

}

assets-dec-onlyif-deposit: “if the assets of a user A are decreased after a transaction, then that transaction must be a deposit() where A is the sender”

“for all reachable states s, and for all transactions T, either T aborts, or P(s, next(s, T), T) holds”

contrapositive!

Multiple-transition invariants

rule finalize_or_cancel_twice_revert {

env e1, e2 ; bool b1, b2;

if (b1) {

finalize(e1);

} else {

cancel(e1); }

if (b2) {

finalize@withrevert(e2);

} else {

cancel@withrevert(e2); }

assert lastReverted;

}

vault/finalize-or-cancel-twice-revert: “a finalize() or a cancel() transaction aborts if performed immediately after another finalize() or cancel() transaction”

“for all reachable states s, and for all sequences of transactions T= T1,…,Tn,

either some Ti aborts, or P(s, next(s, T), T) holds”

Metamorphic properties

rule withdraw_additivity {

env e1, e2, e3;

uint v1, v2;

storage initial = lastStorage; // save the current storage

require e1.msg.sender == e2.msg.sender == e3.msg.sender ;

withdraw (e1, v1);

withdraw (e2, v2);

storage s12 = lastStorage;

​

withdraw (e3, v1 + v2) at initial;

storage s3 = lastStorage;

​

assert s12[Bank] == s3[Bank];

}

withdraw-additivity: “two successful withdraw() of n1 and n2 units of token T performed by the same sender are equivalent to a single withdraw() of n1+n2 units of T”

Properties involving multiple finite sequences of transactions

Non-expressible properties

Properties not expressible in Certora and MVP… but addressable with other tools

• “Eventually a state that satisfies certain conditions is reached” (liveness)

price-bet/eventually-balance-zero: “eventually the contract balance goes to 0”

bank/no-frozen-credits: “if the credits are strictly positive, ∃ user able to reduce them”

vault/finalize-before-withdraw-revert: “a finalize() called before a withdraw() always reverts”

• “In every reachable state, certain users are always able to fire a (fixed) number of transactions to reach a desirable state” (liquidity / enabledness)

• “Some event cannot happen before some other event”

Properties involving arbitrary ∀/∃ quantifiers on transaction parameters

• Reversibility: “Given a state variable q and a function f(), there exists a call to some function g() s.t. the value of q after f() g() is equal to the value of q before the calls”

​

∃f . (〈f()〉〈g()〉balance(A)) >〈f()〉balance(A)

∃g . (〈f()〉〈g()〉q ) ＝ q

∀f . ∃g . (〈f()〉〈g()〉balance(A)) ≥ balance(A)

• Front-running: “User A can call a function f() s.t. balance(A) after f() g() is greater than balance(A) after only g()”

• Attack-defence: “For any call to a function f(), user A can make a call to a function g(), s.t. balance(A) after f() g() is greater or equal to balance(A) before the calls”

MEV attacks

Mempool

Blockchain

MEV attacks

Mempool

Blockchain

ideally: fair ordering

MEV attacks

Mempool

Blockchain

reorder & drop tx

MEV attacks

Mempool

Blockchain

front-run users’ tx

MEV attacks

Mempool

Blockchain

insert tx and “sandwich” users’ tx

MEV attacks

Mempool

Blockchain

Rational players exploit users’ tx to gain $$$

… usually, to the detriment of users’!

MEV

Conclusions

Folklore knowledge:

“Move is better suited than Solidity for verification”

… Is that true?

From our comparative analysis:

• Overall, yes, … although
• Certora (currently) has more functionalities than the Move Prover
• Many relevant properties (“economic”) are still not expressible!

References

• M. Bartoletti, S. Crafa, E. Lipparini. Formal verification in Solidity and Move: insights from a comparative analysis. FMBC, 2025
• M. Bartoletti, R. Zunino. A theoretical basis for MEV. Financial Cryptography, 2025
• M. Bartoletti, R. Marchesin, R. Zunino: DeFi Composability as MEV Non-interference. Financial Cryptography, 2024
• S. Chaliasos, M. A. Charalambous, L. Zhou, R. Galanopoulou, A. Gervais, D. Mitropoulos, B. Livshits: Smart Contract and DeFi Security Tools: Do They Meet the Needs of Practitioners? ICSE 2024