# Move prover: Complex tutorial of formal verification for Sui move

**URL:** <https://forums.sui.io/t/move-prover-complex-tutorial-of-formal-verification-for-sui-move/1812>\
**Category:** Move\
**Tags:** feature\
**Created:** [January 3, 2023, 7:17am UTC](https://forums.sui.io/t/move-prover-complex-tutorial-of-formal-verification-for-sui-move/1812 "2023-01-03T07:17:09Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![IceFox](https://dub1.discourse-cdn.com/sui/user_avatar/forums.sui.io/icefox/32/1003_2.png) [@IceFox](https://forums.sui.io/u/IceFox)\
**Post date:** [January 3, 2023, 7:17am UTC](https://forums.sui.io/t/move-prover-complex-tutorial-of-formal-verification-for-sui-move/1812/1 "2023-01-03T07:17:09Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![lucy2020111111](https://dub1.discourse-cdn.com/sui/user_avatar/forums.sui.io/lucy2020111111/32/981_2.png) [@lucy2020111111](https://forums.sui.io/u/lucy2020111111)\
**Post date:** [January 4, 2023, 1:34am UTC](https://forums.sui.io/t/move-prover-complex-tutorial-of-formal-verification-for-sui-move/1812/2 "2023-01-04T01:34:17Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![peter](https://dub1.discourse-cdn.com/sui/user_avatar/forums.sui.io/peter/32/984_2.png) [@peter](https://forums.sui.io/u/peter)\
**Post date:** [January 4, 2023, 1:38am UTC](https://forums.sui.io/t/move-prover-complex-tutorial-of-formal-verification-for-sui-move/1812/3 "2023-01-04T01:38:32Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![awelc](https://avatars.discourse-cdn.com/v4/letter/a/b5e925/32.png) [@awelc](https://forums.sui.io/u/awelc)\
**Post date:** [February 27, 2023, 6:05pm UTC](https://forums.sui.io/t/move-prover-complex-tutorial-of-formal-verification-for-sui-move/1812/7 "2023-02-27T18:05:26Z")

</div>

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.