Complete examples of program correctness proofs
You will find a collection of proof techniques illustrated with poofs of small programs in the following paper:

Inductive Methods for Proving Properties of Programs, Manna, Ness, Vuillemin, CACM 16-8, August 1973.

It is made available on the web by one of the authors. It is also the first paper I ever read on the subject, and I remember enjoying it.

But I would expect the literature, on and off the web, refereed papers, textbooks and other sources. to include a considerable number of such proofs, considering that today people are working on the proofs of real program (such as compilers), with the help of mechanized proof systems.

OF course, you are aware that there is no such thing as correctness in an absolute sense. Correctness is defined only with respect to some specification, i.e. to some predicate in a logic that can also express the meaning of programs
(or whatever part of it is relevant).

Of course, there are different ways of defining the semantics of a program. So one might expect to have proof techniques that vary accordingly.