Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes.