Proof of correctness of A star search algorithm
Check the original paper which talks about its correctness - 

Hart, Peter E., Nils J. Nilsson, and Bertram Raphael. "A formal basis for the heuristic determination of minimum cost paths." Systems Science and Cybernetics, IEEE Transactions on 4.2 (1968): 100-107.

See especially Section II and Theorem 1.