Classification, one of the most commonly applied algorithmic techniques in data mining, involves assigning a class label to observations based on previously seen data. Among the most ubiquitous and well-known approaches to classification is K-nearest neighbor ( \(K\) NN) search, which predicts the class label for a query by determining the plurality class of its K-nearest data points. In this paper, we present a mechanically verified implementation of a K-nearest neighbors classification algorithm in the Coq  proof assistant, a powerful formal verification tool. Formally certifying the implementation, by proving that it meets its specification, provides a strong guarantee and high confidence that the classifier actually produces results in the expected manner. Given the conceptually simple nature of the \(K\) NN algorithm, this serves as a good baseline for developing specification and verification techniques for machine learning implementations.