Deep Dive into Move's Built-in Formal Verification: Technical Discussion

General
1

I’m interested in understanding the formal verification capabilities that are built into the Move programming language, particularly for theoretical mathematical research and proofs. Specifically, I’m looking to understand:

  1. What specific properties can be formally verified using Move’s built-in verification system? I’m curious about both the practical smart contract properties and any theoretical mathematical properties.

  2. How does Move’s verification system compare to established theorem provers like Coq and Lean? What are the key differences in their approaches and capabilities?

  3. What is the underlying logical foundation of Move’s verification system? I’m interested in understanding the theoretical framework it’s built upon.

  4. Can the system be used to prove arbitrary mathematical theorems, or is it primarily focused on program correctness properties?

If anyone has experience working with Move’s formal verification system or knows of relevant research papers/documentation that explore these aspects in depth, I’d greatly appreciate the references.

Note: I’m particularly interested in understanding how this could be applied to pure mathematical research beyond just smart contract verification.

Would anyone here be able to shed some light on these technical aspects of Move’s verification system?​​​​​​​​​​​​​​​​

1 Like
2

Hi @Wenitte,
in theory the Move Spec Language and the Move Prover are expressive enough to prove general mathematical statements.
However, Move is resource-oriented language, specifically designed to implement contracts and manage resources in a safe way.
So Move is a good option for proving properties of contracts but not necessarily the best for general mathematical statements.

To prove properties of algorithms (in general), I would recommend automated reasoning tools using deductive verification like Dafny or Why3.

TO go further, there are several fantastic tools (and theories) dedicated to implementing general theories (sets, etc) and prove mathematical statements, and they are usually called Theorem provers.
Here is a partial list of theorem provers:

If you are interested in an introduction to machine assisted proof of theorem, there is a nice talk by Terence Tao (Fields medal 2006, which is the “Nobel prize in Mathematics”).
There is a corresponding article here which is very nice to read too.

TL;DR
There are rich and extensive libraries of mechanised mathematical proofs (in Lean, Coq, Isabelle) and mathematicians are using them to build proofs of new theorems on top of them.

2 Likes