Move prover: Complex tutorial of formal verification for Sui move

Currently I’m working on an over collateral lending platform. The logic here is somehow relatively complex. I want to make my contract safer by writing formal verification on my code. But I can’t find a good tutorial for writing Move prover on SUI. Any suggestions?

20 Likes

you can join the community of sui, discuss the questions.

8 Likes

discord sui , you can ask the questions to it,maybe the assistant will answer you

7 Likes

Support for Sui in the Prover is still in the works. At this point, you can write and verify specifications that do not involve Sui native functions. There is also limited support for reasoning about aborts when transferrin, sharing or freezing objects. You can see example of specs not involving native functions in the coin module and the other supported features in the prover_test module.

4 Likes