[Docs] Document Move Prover use on Aptos.dev, migrate Move Lang spec

[clay-aptos]

Aptos Documentation Issue

Location

What are the existing URLs containing the issue, if any?

Will be a new page linked from the install doc:
https://aptos.dev/cli-tools/install-move-prover

Where should this information land if new? (Start Aptos, Build Apps, Run Nodes, Reference, etc.)

Move section, with reciprocal links from install docs.

Description

How would you describe the issue?

We cover install only and leave usage elsewhere:
https://github.com/move-language/move/blob/main/language/move-prover/doc/user/prover-guide.md

Further, the invaluable Move language specification is also hard to find:
https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md

We are discussing migrating those contents to Aptos.dev. In doing so, we should also link to external resources we find valuable, such as:
https://osec.io/blog/2022-09-16-move-prover/
https://www.certik.com/resources/blog/2wSOZ3mC55AB6CYol6Q2rP-formal-verification-the-move-language-and-the-move-prover

In fact, @junkil-park has a fantastic list of such docs internally titled "Awesome Move Prover" we should take public in the form of a Supporting documentation section in our user docs.

Junkil also has a tutorial in mind. Let's do this thing!

Audience

Additional context

[clay-aptos]

Related, I still need to sweep through the site and replace links to the Move book and tutorial with our versions.

[clay-aptos]

Related, I still need to sweep through the site and replace links to the Move book and tutorial with our versions.

Thanks to @xindingw for getting the ball rolling in the Move reference docs!
#7425

[clay-aptos]

Wow! @rahxephon89 has started a Prover Guide in the following PR we should link to:
#7296

[rahxephon89]

Wow! @rahxephon89 has started a Prover Guide in the following PR we should link to: #7296

Hi @clay-aptos , this guide is currently specifically for the internal users who are developing the framework. But I will check with the team on a general prover guide that can be added to aptos.dev

[clay-aptos]

Per the team, we should recommend this as why to use the Move Prover:
https://www.certik.com/resources/blog/1NygvVeqIwhbUk1U1q3vJF-the-move-prover-quality-assurance-of-formal-verification

So I am adding in the following PR and also strongly recommending use of the Move Prover:
#7468

[wrwg]

Per the team, we should recommend this as why to use the Move Prover: https://www.certik.com/resources/blog/1NygvVeqIwhbUk1U1q3vJF-the-move-prover-quality-assurance-of-formal-verification

So I am adding in the following PR and also strongly recommending use of the Move Prover: #7468

No this is definitely not a blog why one should use the Move Prover, this is just one aspect of how to use it. There are other blogs (from OtterSec, MoveBit, and Certik as well) which are better for making this argument. @junkil-park has the list of those.

[clay-aptos]

Per the team, we should recommend this as why to use the Move Prover: https://www.certik.com/resources/blog/1NygvVeqIwhbUk1U1q3vJF-the-move-prover-quality-assurance-of-formal-verification
So I am adding in the following PR and also strongly recommending use of the Move Prover: #7468

No this is definitely not a blog why one should use the Move Prover, this is just one aspect of how to use it. There are other blogs (from OtterSec, MoveBit, and Certik as well) which are better for making this argument. @junkil-park has the list of those.

I misspoke. Please see the PR:
#7468

[clay-aptos]

@junkil-park , I have added @saharct as Christian wants to help with the Move Prover documentation.

@wrwg , here is a start on updating links to our versions of the Move Book and Tutorial:
#7621

Please note, I am not sure how to handle the links in the reference files, such as the one at the top of:
https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-framework/doc/aptos_coin.md

If we need to update those, perhaps we can instead employ your doc templates, for example:
https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-stdlib/doc_template/references.md

[clay-aptos]

Hi @junkil-park and team, here is the PR to add relevant links from the internal Awesome Move Prover list to the Install Move Prover page for now as supporting resources:
#7623

Please note, I removed the MoveBit link as a 404:
https://blog.movebit.xyz/post/move-prover-tutorial-part-1.html

Please let me know what you think.