Lessons from setting up the Move Prover on a production Aptos DeFi codebase — the dependency hell, the false positives from signed division semantics, the BigOrderedMap wall, and the spec-writing tricks that actually work.
I've been doing formal verification on Sui Move using Certora's prover, and the natural next question was: what does the tooling look like on Aptos?
Aptos Move has a built-in formal verification tool called the Move Prover. It ships with the Aptos CLI, uses the Boogie intermediate verification language and Z3 SMT solver under the hood, and lets you write specifications directly alongside your Move code using the Move Specification Language (MSL).
The promise is powerful: you write mathematical properties about your contract's behavior, and the prover either confirms they hold for all possible inputs or gives you a counterexample. No fuzzing randomness. No missing edge cases. Mathematical proof.
But the reality of using it on a production DeFi codebase? That's where things get interesting.
Before diving into the war stories, here's how the Move Prover works at a high level:
Specs live in .spec.move files alongside your source, or inline in the same file. They're written in MSL — a declarative language that looks like Move but operates at the mathematical level. You write ensures, aborts_if, requires, and invariant clauses, and the prover checks them exhaustively.
The aptos move prove command is built into the Aptos CLI, but it needs two external tools: Boogie (a .NET tool) and Z3 (the SMT solver). This is where most people give up. Let me save you the pain.
The Move Prover is extremely picky about tool versions. At the time of writing (Aptos CLI v8.x), the constraints are:
| Tool | Required Version | What Happens If Wrong |
|---|---|---|
| Boogie | ≤ 3.5.1 | "cannot extract version" error |
| Z3 | ≤ 4.11.2 | "unsupported Z3 version" error |
| .NET SDK | 8.0.x | Boogie fails to launch |
If you install the latest versions of any of these, the prover will reject them. The latest Boogie is 3.5.6, the latest Z3 is 4.15+, and the latest .NET is 10.0 — all too new.
Here's the exact sequence that works:
Critical: All three environment variables (DOTNET_ROOT, BOOGIE_EXE, Z3_EXE) must be set for every invocation. Miss one and you get cryptic errors like "cannot extract version" or "boogie not found". The DOTNET_ROOT is especially sneaky — if you have .NET 10 as your system default, Boogie will try to use it and fail silently.
Once everything is wired up, test on a simple module first:
If you see "generating 10 verification conditions" and Z3 starts solving them, your setup works. Any errors before that point are dependency issues.
The Move Specification Language is surprisingly expressive. Here are the key constructs you'll use:
Pragmas are your escape hatches. In a large codebase you'll use them constantly:
In the codebase I was analyzing, I found 37 functions with pragma verify = false. That's not unusual for a production system — it means the team verified what they could and explicitly marked what they couldn't. It's honest, and it tells you exactly where the formal verification gaps are.
Auditor's perspective: Those pragma verify = false directives are a roadmap. Every skipped function is a potential verification target. If you're doing a security audit with formal verification, start by listing every pragma verify = false and asking: why was this skipped, and can we write a spec for it now?
Spec functions (spec fun) are pure mathematical functions that exist only at the specification level. They never execute on-chain. They're your building blocks for expressing properties:
The key constraint: spec functions must be pure. No side effects, no mutable references, no loops that modify state. This sounds simple until you hit real code.
This was the first major hurdle. I wanted to write a spec like:
Simple, right? But get_balance() internally iterates over a secondary assets table using a loop that mutates a local accumulator. The prover rejected it immediately:
Error: Spec functions cannot call impure runtime functions. Any function that contains loop mutations, mutable references, or side effects is off-limits in ensures, requires, or invariant clauses.
The solution? Go lower. Instead of calling the runtime's convenience function, reach directly into the data structures using spec-native accessors provided by the Aptos framework.
The Aptos framework defines spec-level functions that bypass runtime code entirely:
Using these, I could reconstruct the balance check at the spec level:
Pattern: When a runtime function is impure (loops, mutations), write a spec fun that reads the same data using table::spec_get, aggregator_v2::spec_get_value, and other spec-native accessors. You're building a pure mathematical mirror of the runtime logic.
A note on that 9223372036854775808 magic number: it's 263. Many Aptos DeFi protocols store signed integers as offset-encoded u64 values inside Aggregators (since Aggregators only support unsigned types). The offset maps i64::MIN..i64::MAX to 0..u64::MAX. In your spec, you need to manually undo this encoding to reason about the actual signed value.
This one stopped me cold. I had a working spec, the types checked, the logic was sound — but the prover crashed during Boogie code generation.
The issue: the module I was verifying used BigOrderedMap, a relatively new Aptos data structure that uses enum variants internally. The Move Prover's Boogie translation doesn't handle these correctly yet — it generates malformed BPL code for enum variant pattern matching.
This isn't a user error. It's a known limitation of the current prover. Any module that touches BigOrderedMap (or similar enum-heavy data structures) will hit this wall.
Workaround: If your target function doesn't directly use BigOrderedMap but shares a module with functions that do, you can use --filter function_name to verify only specific functions. But if the function you care about transitively touches a BigOrderedMap, you're stuck. The only real fix is upstream in the prover.
This is where the difference between Sui and Aptos formal verification becomes stark. On Sui, Certora's prover handles the entire Sui object model including dynamic fields. On Aptos, the built-in prover struggles with newer standard library types. The tradeoff: Aptos has a free, built-in prover with deep MSL integration; Sui requires an external tool (Certora) but with broader data structure support.
This was my favorite discovery. I ran the prover on an i64_math utility module that had existing specs for ceiling division and floor division. The prover reported 4 post-condition violations. My first reaction: we found bugs!
Not so fast.
Here's a simplified version of what the code does:
The prover claimed this fails for ceil_div(-1, 2). It computed result = -1, giving -1 * 2 = -2, which is NOT >= -1. Violation!
But wait. What does -1 / 2 actually produce in Move?
The Move runtime uses truncation division (round toward zero), like C, Rust, and Java. But the Move Prover's Z3 backend models integer division as floor division (round toward negative infinity), like Python and standard mathematics.
For positive numbers, these are identical. For negative numbers, they diverge:
| Expression | Truncation (Move runtime) | Floor (Prover's model) |
|---|---|---|
-1 / 2 |
0 | -1 |
-3 / 2 |
-1 | -2 |
-7 / 2 |
-3 | -4 |
7 / 2 |
3 | 3 |
All four "violations" the prover reported were false positives caused by this division semantics mismatch. The existing unit tests in the codebase all pass — the runtime behavior is correct.
This is a real footgun for auditors. If you're using the Move Prover to verify signed arithmetic and you see post-condition violations on division, check the division model before filing a bug. Trace the counterexample manually using truncation semantics. The prover might be wrong about how the code actually behaves.
How to confirm: Take the prover's counterexample values. Manually compute the expression using truncation division (round toward zero). If the postcondition holds under truncation but not under floor division, it's a prover false positive, not a real bug.
Beyond catching arithmetic bugs, the real power of formal verification in DeFi is proving protocol-level invariants. Here are generic patterns that apply to most perpetual futures or margin-trading protocols on Aptos:
The challenge is always the same: the spec_* helper functions need to be pure, so you end up reconstructing complex balance lookups using spec-native accessors. For simple modules, this is tractable. For modules with deeply nested data structures or complex iteration patterns, you may need to use pragma opaque to abstract away the internals and spec the function's external contract instead.
Having used both, here's my honest comparison:
The Aptos prover is better for quick, targeted verification of specific functions — especially math utilities, access control checks, and abort conditions. Certora's Sui prover is better for protocol-wide invariants where you want to verify a property across every state-mutating function with a single parametric rule.
Neither is perfect. Both are worth learning if you're serious about Move security.
--filter. Don't try to verify an entire complex module on day one. Use aptos move prove --filter module_name to isolate what you can verify, and expand from there.pragma verify = false is your audit roadmap. Every skipped function tells you where the team hit a verification wall. These are the functions most likely to have unverified edge cases — and where manual review should focus.spec fun mirror using table::spec_get, aggregator_v2::spec_get_value, and other spec-native accessors.i64; Move uses truncation. Any spec involving negative number division will produce false positives. Always verify counterexamples manually.The Aptos Move Prover is a powerful tool that's one or two upstream fixes away from being genuinely production-ready for complex DeFi codebases. Even with its current limitations, it can verify math utilities, access control invariants, and abort conditions with mathematical certainty. If you're auditing Aptos contracts, it's worth adding to your toolkit — just bring patience for the setup.
Disclaimer: This article is for educational purposes only. Protocol names and specific implementation details have been generalized. The findings and observations described are from real formal verification work on production Aptos DeFi codebases, but this article does not constitute security advice. Formal verification proves properties about a mathematical model of the code — it does not guarantee the absence of all bugs. The signed division semantics mismatch described here is based on observed behavior with Aptos CLI v8.x and may be resolved in future versions. Always combine formal methods with manual review, fuzzing, and testing. If any information here is outdated or incorrect, please reach out on X so I can update this article accordingly.