Your algorithm has a typo. The inner loop should start $j := i + 1$ and go to $n$. Notice that after iteration $i$ of the outer loop, the largest $i$ elements are sorted correctly at the end of the list. Prove this fact, which I will call $(*)$.
We also have termination, by finiteness of both loops (and no modification of $i, j$ other than incrementation).
You can then use induction on $(*)$ to argue that if the largest elements are sorted correctly at indices $n-i, ..., n-1$, then the next iteration of the loop will correctly place the $n-1-i$ largest element at index $n - 1 - i$, preserving order.
Edit:
Claim: On the ith iteration of the outer loop, the largest $i$ elements will be sorted correctly (at the end of the array).
Proof: By induction on $n \in \mathbb{N}$. Consider the base case of $n = 1$. Let $x$ be the largest element in the array. By the algorithm, if $x$ is unique, $x$ is swapped on each iteration after being discovered initially. It is then placed at the end. If $x$ is not unique, then there exists a second copy of it and no swap will occur. However, the second copy will then be swapped. This process continues, so the last occurrence of $x$ will be moved to the end of the array. The theorem thus holds at $i = 1$.
I assume the theorem holds true up to an arbitrary integer $k$ such that $1 < k < n$ and prove true for the $k+1$ case. Let $y$ be the $k+1$ largest element in the array. We consider the reduced case of examining the first $n - k - 1$ elements. By the inductive hypothesis, $y$ will be correctly placed at the end of this sub-array. As $y$ is no bigger than the $k$th largest element, $y$ will not be moved further down into the array. The $k+1$ case thus holds.
And so the claim holds true by the principle of mathematical induction.
Let's say we want to find primes by certain algorithms (called primality tests)
A sound primality test will never say that a number is prime when it is composite (but it may fail to detect some primes as such; it may also sometimes fail to HALT)
A complete primality test will never say that a number is composite when it is prime (but it may fail to detect some composites, thus produceing "pseudo-primes" or it fails to HALT)
A paritally correct primality test may sometimes fail to give an result at all (i.e., fail to HALT). But if it returns a result it is correct: If it says prime, the input is prime, and if it says composite, the input is composite.
A (totally) correct primality test will always halt, and it will always return the correct answer.
Best Answer
If you want to eliminate any hand-waving, then use a mechanized theorem prover. A significant book series in this area that's also available online is Benjamin Pierce's Software Foundations series. This series teaches you how to use the proof assistant Coq, the system used for (among many other things) formally verifying the CompCert C compiler, for computer science problems including algorithm verification. From there Coq libraries like YNot and the research/publications around them would be a place to look.
There are also mechanized theorem provers or related tools that take different approaches. Things like Frama-C, Why3, Alloy, Spin, Ada SPARK, the $\mathbb{K}$ Framework, NuPRL, Isabelle/HOL, Twelf, TLAPS, Welder/Inox and many others. These approach different aspects of the problem with different approaches and different levels of ambition and usability. For example, to prove something about a program, you need to have a semantics for the programming language. Simplifying the creation of programming language semantics is the goal of the $\mathbb{K}$ framework meanwhile Ada SPARK is a large fragment of Ada with a formal semantics. Specifying the semantics of C and assembly in Coq was a huge part of the CompCert project. Given a semantics, you then need some way of giving a specification of your program and generally connecting the source code. Frama-C does this for C (and there are variations in that suite for other languages). Of course, stating what you expect is different from proving that it holds. Proof assistants like Coq, Twelf, Isabelle/HOL, and TLAPS allow very complicated theorems to be proven but require a fairly high level of expertise to use in real world cases. These also take different approaches using either constructive type theory, classical higher-order logic, or set theory. In many cases, what needs to be proven is relatively simple and can be fully automated. Tools like Welder/Inox coordinate automatic theorem provers to deal with these. Sometimes its just too expensive/difficult to get (and crucially maintain) a full proof of correctness. Model checkers like Spin and Alloy can be used to exhaustively check the state space of the program (or an abstraction thereof) at least to some depth. These can often find defects, and in some cases may be able to fully check the state space. These are much easier to use but they don't give the same guarantees and can take huge amounts of computation. In practice, they are often used to verify protocols rather than the actual code to minimize the state space. A different approach to trying to prove code correct is to extract the program from a proof. NuPRL is one of the oldest, still living systems that focuses on this approach, but this can be done with Isabelle/HOL and Coq as well. Some systems like Why3, Welder, and Isabelle are more frameworks meant to help join tools together. There are many other alternatives to the tools that I've listed in each of their niches.