Cliff Jones has written about the early history of program verification. Correctness proofs for algorithms have been given since Euclid. In the early 19th century, Charles Babbage already contemplated the verification problem for a set of machine instructions. The formal concept of an algorithm was introduced and developed by Alonzo Church, Alan Turing, Emil Post, Jacques Herbrand, Kurt Goedel, and Stephen Kleene. Assertional correctness proofs for flowcharts were first carried out by Herman Goldstine and John von Neumann in 1947. Alan Turing, in 1949, also developed a method of assertional correctness, including considerations of overflow and termination.

John McCarthy in a 1961 paper A Basis for a Mathematical Theory of Computation":http://www-formal.stanford.edu/jmc/basis.html outlines a discipline of program correctness by developing

• A language of recursive functions and conditionals (including an ambiguous choice operator).
• A formal axiomatic semantics for the language
• A framework for defining new datatypes
• A theory of conditional expressions
• A method of recursion induction for verifying properties of recursive programs
• A way of mapping flowcharts to recursive functions, developed in Recursive Functions of Symbolic Expressions and their Computation by Machine (Part I)
• A suggestion for computer verification of proofs of programs, asserting `the potential applications for computer-checked proofs are very large. For example, instead of trying out computer programs on test cases until they are debugged, one should prove that they have the desired properties.'

Assertional verification was rediscovered and further developed by Robert Floyd and Peter Naur in the mid-1960s. Floyd developed a rigorous approach for introducing assertions (including loop invariants) in the first-order predicate calculus, for characterizing program statements in terms of strongest post-conditions, introducing methods for proving both partial and total correctness, and for generating verification conditions.

Tony Hoare, in 1969, presented an axiomatic framework for programming language semantics and for program correctness proofs based on triples consisting of the pre-condition, the program statement, and the post-condition, and syntactic rules of inference.