Bernny Velasquez, Jessica Herring, and Nadeem Hamid. 2024. Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm. In Anais do XXVII Simpósio Brasileiro de Métodos Formais, dezembro 04, 2024, Vitória/ES, Brasil. SBC, Porto Alegre, Brasil, 139-152.