Formalized Burrows-Wheeler Transform

The Burrows-Wheeler transform (BWT) is an invertible lossless transformation that permutes input sequences into alternate sequences of the same length that frequently contain long localized regions that involve clusters consisting of just a few distinct symbols, and sometimes also include long runs of same-symbol 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 the BWT 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.