Movement has merged a major formal verification infrastructure into its aptos-core repository, introducing a complete Lean 4 bytecode model and refinement proof framework. The update, contributed by the core development team, adds rigorous mathematical specifications for Move VM semantics alongside automated differential testing.
The new system defines core Move abstractions—`Value`, `Instr`, `State`, `Step`, `Native`, and `Programs`—in Lean 4, with special focus on bytecode-level semantics including real disassembly-backed programs. Refinement proofs establish correctness relationships between the formal model and the actual VM implementation, including a kernel-checked theorem for `vector::contains` operations verified against the standard library.
A differential testing harness (`move-lean-difftest`) automatically compares the real Move VM to the Lean evaluator on shared test oracles across vector operations, binary canonical serialization (BCS), and hash functions. This bidirectional verification approach—comparing Rust and Lean implementations directly—enables early detection of semantic divergences and strengthens confidence in protocol correctness.
The framework includes comprehensive documentation and tooling: `lake build` compiles the Lean proofs, the `difftest.sh` script runs all verification suites, and supporting Move golden tests validate byte-level consistency. The repository also registers `AptosStd` layouts for cryptographic primitives like Ristretto and SHA3-512, ensuring formal specs align with production implementations.
Developers can verify the proofs locally by installing Lean 4 (4.24.0) via `elan` and running the Lake build system. The complete runbook and bytecode model roadmap are documented in the repository's formal verification README files, making this infrastructure accessible for ongoing protocol development and third-party audits.