Shunting-yard algorithm - proof
The shunting-yard algorithm was introduced in Dijkstra's article Making a Translator for ALGOL-60 (APIC Bulletin no7, 1961; see this PDF, from p.22; also published in Annual Review in Automatic Programming, 7:3&ndash;11, 1963 and available from Science Direct if your institution has a subscription).  Pages 7&ndash;9 of the article (pp.28&ndash;30 of the PDF) explain how the algorithm works and argue its correctness. It's not a formal proof but it looks like it contains everything you should need to produce one.