Convolutional codes are widely used for error correction in domains such as data transfer and data storage. These algorithms have an extremely wide range of applicability, including in areas where a high level of assurance is necessary. It is a shame, therefore, that very little work has been done on the formal verification of convolutional codes using interactive theorem provers. In this talk, I provide the background information necessary to understand convolutional codes, motivate the need for a formally verified implementation of convolutional codes, provide a summary of the current work that has been done in this area, and outline the steps that will need to be taken to produce a formally verified error correcting code algorithm.