Kleene algebra (KA) is an algebraic system that captures properties of several important structures arising in Computer Science like automata and formal languages, among others. In this paper we present a formalization of regular languages as a KA in the COQ theorem prover. In particular, we describe the implementation of an algorithm for deciding regular expressions equivalence based on the notion of derivative. We envision the usage of (an extension of) our formalization as the formal system in which we can encode and prove proof obligations for the mechanization and automation of the process of formal software verification, in the context of the Proof Carrying Code paradigm.