The Burrows-Wheeler transform (BWT) is a core algorithm used in data compression due to its ability to enhance the effectiveness of subsequent entropy coding steps, such as data compression and text search. BWT is an invertible lossless transformation that permutes sequences into alternate sequences that frequently have long runs of repetitions. As a consequence, the BWT is used in a wide range of tools, from everyday file compression software, such as bzip2, to highly sophisticated bioinformatics tools, such as DNA sequencers, where an efficient encoding of genomic sequences is essential. As such, ensuring the correctness of BWT and its inverse is critical. In this paper, we present the first formal verification of both the BWT and its inverse. Our verification efforts are conducted in Isabelle/HOL. Building on a recent formalization of the suffix array construction algorithm, we provide a mechanized proof of correctness, invertibility, and termination for both transformations. By doing so, we address the gap in the formal verification of compression algorithms, ensuring that the BWT can be safely deployed in critical applications such as genomic data analysis. This work thereby also provides the necessary foundation for verifying the various algorithms for compression and text search that operate on BWT-transformed sequences.