An algorithm is correct if it produces the expected output for each input.
An algorithm is only partially correct if may not terminate. Otherwise it is totally correct.
Model checking allows the formal verification of algorithms with finite inputs. test every possible input.
Check the parts of the algorithm using theorem provers.