A Programmer's Mental Model for Proving

This paper presents an approach to formal verification in Lean based on modeling program behavior through paths in a control-flow graph. Using the Averroes Lisp parser as a case study, it expresses path conditions as theorem hypotheses and specifies the semantics of each path’s returned value in the theorem’s conclusion.