We propose a verified executable Scala backend for ASN1SCC, a compiler for ASN.1/ACN. ASN.1 is a language for describing data-structures, widely employed in ground and space telecommunications. ACN can be used along ASN.1 to describe complex binary formats and legacy protocols. To avoid error-prone and time consuming manual writing of serializers, we show how to port an ASN.1/ACN code generator to generate Scala code. We then enhance the generator to emit not only the executable code but also strong enough preconditions, postconditions, and lemmas for inductive proofs. This allowed us to verify the resulting generated annotated code using Stainless, a program verifier for Scala. The properties we prove include absence of runtime errors, such as out-of-bound accesses or divisions by zero. We prove the invertibility of the decoding and encoding functions used in the base library, showing that decoding yields the encoded value back. We also prove the invertibility for records in the generated code and establish key steps towards proving invertibility for sums and arrays.