This is the oral component of my confirmation of candidature. My research topic is the formal verification of convolutional codes and other related codes such as turbo codes. These algorithms are in widespread use, but they have only been formally verified to a limited extent. I have been using the HOL4 interactive theorem prover to produce formalizations of these algorithms. I have produced the first formalization of convolutional codes with arbitrary generator polynomials. I have also produced the first formalization of the Viterbi decoder, and proved that it satisfies a correctness property. Finally, I have produced the first formalization of the process of converting a convolutional code into state machine form, proved that the state machine representation is equivalent to the original representation, and proved that the state machine which is generated is well-formed. My next goal is to formally verify turbo codes.