ABSTRACT: High-integrity software is software whose failure may lead to catastrophic consequences. To develop software to such a high standard, formal methods have been introduced into the software development process. Programs' behaviours and the properties of their output are defined by their specification. Programs that have been formally verified guarantee adherence to said specification. Permutations are a common type of mapping function in programming. The repeated application of a permutation to an element yields sequences with repetition. This phenomenon is known as a cycle of a permutation. Permutations containing only one non-trivial cycle are known as cyclic permutations. Decomposing permutations into cyclic permutations is used in various algorithms, ranging from sorting to error correction. This thesis explores the development a formally verified algorithm for decomposing permutations into cyclic permutations with disjoint cycles. For this, the interactive theorem prover Rocq Prover is employed. The mathematical definitions and properties that the algorithm must adhere to are transferred into Rocq's Gallina specification language. This thesis presents a proof sketch for showing that the algorithm is correct. One of the results of this thesis is a usable, however not yet fully formally verified, algorithm for decomposing permutations into cyclic permutations with disjoint cycles. The specification and proof sketch laid out by this work will proof useful for future scientific works.