This paper presents a polynomial-time algorithm for correcting t errors in classical binary Goppa codes defined by square-free degree-t polynomials. The algorithm is simpler than Patterson's algorithm and is based on a proof of a Reed–Solomon decoder. The algorithm is implemented in Sage, with formal verification of all theorems. The paper also discusses the use of decoding in the Classic McEliece cryptosystem, including reliable recognition of valid inputs. The paper begins by introducing the McEliece cryptosystem and the role of Goppa decoding in it. It then explains how to recover a polynomial from its values, a process known as interpolation. The algorithm for interpolation is followed by an algorithm for finding approximants, which is used in the decoding process. The paper then discusses interpolation with errors, which is used to correct errors in the code. The paper also covers Reed–Solomon codes and their relation to Goppa codes. It explains how to decode Reed–Solomon codes and how this can be used to decode Goppa codes. The paper then presents an algorithm for binary-Goppa decoding, which is based on the interpolation and approximant algorithms. The algorithm is tested on random inputs and is verified for correctness. The paper also discusses the history of Goppa decoding and its relation to other decoding algorithms. It explains how the algorithm for binary-Goppa decoding is derived from the algorithm for Reed–Solomon decoding. The paper concludes by discussing the importance of simplicity in decoding algorithms, as well as the benefits of formal verification in post-quantum cryptography.This paper presents a polynomial-time algorithm for correcting t errors in classical binary Goppa codes defined by square-free degree-t polynomials. The algorithm is simpler than Patterson's algorithm and is based on a proof of a Reed–Solomon decoder. The algorithm is implemented in Sage, with formal verification of all theorems. The paper also discusses the use of decoding in the Classic McEliece cryptosystem, including reliable recognition of valid inputs. The paper begins by introducing the McEliece cryptosystem and the role of Goppa decoding in it. It then explains how to recover a polynomial from its values, a process known as interpolation. The algorithm for interpolation is followed by an algorithm for finding approximants, which is used in the decoding process. The paper then discusses interpolation with errors, which is used to correct errors in the code. The paper also covers Reed–Solomon codes and their relation to Goppa codes. It explains how to decode Reed–Solomon codes and how this can be used to decode Goppa codes. The paper then presents an algorithm for binary-Goppa decoding, which is based on the interpolation and approximant algorithms. The algorithm is tested on random inputs and is verified for correctness. The paper also discusses the history of Goppa decoding and its relation to other decoding algorithms. It explains how the algorithm for binary-Goppa decoding is derived from the algorithm for Reed–Solomon decoding. The paper concludes by discussing the importance of simplicity in decoding algorithms, as well as the benefits of formal verification in post-quantum cryptography.