It has been argued [7], that lazy functional programming languages have a simple semantic definition, which allows formal software development methods to be easily used. If the object of this exercise is seen to be the production of a working program, then the implementation should also be correct before the system may be said to meet its specification. Recent work has shown that such languages can now be efficiently implemented using graph reduction. Because of its concise definition this paper concentrates on Augustsson and Johnsson's G-machine [1] and [2]. Unfortunately, efficiency considerations lead to a complicated implementation, the correctness of which is not immediately obvious. This paper outlines a proof that an implementation similar to Johnsson's is correct with respect to a stack semantics for a simple lazy functional programming language. This semantics has been shown elsewhere [3] to be congruent to the natural standard semantics for the language. The major difference between the method presented here and that of Johnsson is the use of indirection nodes. The paper also furnishes a proof that Johnsson's alternative strategy is correct.