The bubble sort algorithm has been implemented in a functional manner. Then the correctness of the implementation has been formally verified using Coq. Particularly, the files Perm.v and BubbleSort.v is pertinent to the proposal, and the other .v files are preparatory materials used along the way for learning purposes.