The following explanation was given to a math colleague concerning nonstandard models:
if Con(PA) fails in a non-standard model, it means it contains a
“proof of non-standard length” of a contradiction from PA. With a
little work, one can externalise that to some non-well-founded “proof
tree”, which has at each node a possibly-non-standard formula (which
in turn externalises to some not-necessarily-well-founded syntax
tree), where each step will genuinely follow from earlier steps by
some standard rule of proof, but the whole tree will be
non-well-founded, and hence not an actual proof.
Said colleague had the following question regarding this explanation:
I find this non-well-founded approach an enlightening way of viewing incompleteness. I checked in a book by Peter Smith on Goedel’s theorems, but it does not seem to discuss this particular aspect (possibly he views it as equivalent to discussion around 
-completeness). Do you know of any book that would place non-well-foundedness center-stage?
I have been using that example in several of my talks in the last few years! (See, e.g. slide 31 of my talk at WoLLIC last year). I don’t know of this being discussed in any book, but this viewpoint was known to (some) logicians in the mid-20th century.
Mints in 1978 developed his continuous cut-elimination at least in part for application to non-wellfounded proofs; indeed as a result, as he says in the abstract, “this permits us to apply [continuous cut-elimination] in the theory of models”. Some investigation connecting non-wellfounded proof trees and non-standard models has occurred in a (bizarrely titled) 1975 paper of Kriesel, Mints and Simpson, which Mints credited as an inspiration for his continuous cut-elimination.
Since the ’70s I am unaware of further applications/developments between non-wellfounded proofs and nonstandard models, but the former have seen a resurgence of interest in the last 30 years, in particular in computer science.