move-inf

{{ frontmatter(name="move-inf", description="Infer specifications for a Move package") }}

Before doing any work, use TaskCreate to create one task for each **Task:** entry listed below. Then execute them in order, marking each in_progress when you start it and completed when you finish.

{% include "templates/spec_inf_tasks.md" %}

The reference material below supports the tasks above.

{% include "templates/spec_inf_ref.md" %} {% include "templates/verification_ref.md" %}

Task

Run specification inference workflow for current package.