How can I prove algorithm correctness?
In practice, to prove an algorithm you should search a good invariant property for each loop. For example, if you compute in a given order the sum of $n$ integers with a for loop (indexed by $i$), the invariant could be : "At the end of an iteration, the $sum$ variable contains the sum of the $i$ first values". It's  invariant over iterations number and always true, it's easy to prove this by recurrence on the iterations number. Afterwards you can easily conclude that, at the end of the loop, $i=n$ and thus that $sum$ is the expected sum.

Then, there is several levels of strictness, but for simple algorithms we can generally conclude promptly since the correction of the algorithm becomes almost always trivial with all the loops invariants. A very classical approach is to prove before that the algorithm finishes and after that the algorithm is correct when it ends. For complete examples you can look here. For more subtil algorithms, you can also need some mathematical theorems which provide some links beetween objects.

Your example is very close to Misra-Gries algorithm. You can look for the proof of the Misra-Gries algorithm and try to adapt it or you can try to bound the number of times the count of the most frequent number is decreased.

In general, there isn't a systematic way to find if an algorithm produces the expected output or not. Indeed, this systematic way would be an algorithm and such an algorithm can't exist (Rice's theorem).