When I read proof, I assumed you meant you proved your quicksort returned an ordered permutation, but after looking at your webpage, I see you are only claiming

When I read proof, I assumed you meant you proved your quicksort returned an ordered permutation, but after looking at your webpage, I see you are only claiming to have proved termination. Not sure why you posted the github instead of your webpage, as without any explanation this code is nearly unintelligible. It would be interesting to hear an explanation of your example, it really is difficult to decipher. If you are interested in proving things about programs, you may want to check out some mechanical theorem provers such as ACL2, HOL or PVS.