Start with this link: Dafny Insertion Sort. Use the Dafny system in your browser (as that link will give you), or install Dafny within your own VSCode setup (see instructions below). Keep adding requires, ensures, and invariants (etc.) until there are no verification errors remaining.
Add a //README comment at the top describing who you helped (or got help from), and what kind of help. Safe your solution into a file sort.dfy, and upload it at right.