B. Velasquez, J. Herring, and N. Hamid. " Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm", in Proceedings of the 27th Brazilian Symposium on Formal Methods, Vitória/ES, 2024, pp. 139-152.