ABSTRACT. Vehicle-to-Vehicle (V2V) communications is a ``connected vehicles'' standard that will likely be mandated in the U.S. within the coming decade. V2V, in which automobiles broadcast to one another, promises improved safety by providing collision warnings, but it also poses a security risk. At the heart of V2V is the communication messaging system, specified in SAE J2735 using the Abstract Syntax Notation One (ASN.1) data description language. Motivated by numerous previous ASN.1 related vulnerabilities, we present the formal verification of an ASN.1 encoder/decoder pair. We describe generating an encoder/decoder pair, implemented in C, using our internally developed ASN.1 toolset. We define self-consistency for encoder/decoder pairs that approximates functional correctness without requiring a formal specification of ASN.1. We then verify self-consistency and memory-safety using symbolic simulation via the Software Analysis Workbench.