This paper proposes a machine-checked and interface-based formal verification for the k-center problem. This formal architecture is built with four modules (Metric, FiniteSet, Radius, and Feasible). These modules separate the abstract metric view from graph, tree, and Euclidean backends, so that proofs can be reused across these spaces without modification. The algorithms are certificate-based. First, the greedy algorithm returns a farthest-first solution and is also a packing and covering witness. Second, the tree decision routine returns traces that show when a radius is feasible. Third, the graph backend offers multisource breadth-first search oracles that support these proofs. As a result, composable machine-checked proofs of classical results are obtained, and specialized versions for new settings are easy to add. The farthest-first constant factor approximation is formalized with a simple separation invariant. An exact tree oracle, called checkR, is given by binary search over a finite set of radii. A graph formal method is also designed that uses a packing-based witness to show that a target radius is not feasible. The greedy template is also combined with symmetric epsilon coresets, so the constant factor bound is kept under a controlled error from the coreset. For online input, a template is proposed to keep maximal packing. This template provides a radius within a factor of 2 of the best possible radius at each step. The framework is independent of one proof assistant and can be used in Lean. It is built for extension, since capacities and outliers are added by changing only the feasibility part. Low doubling and planar cases reuse the same basic lemmas, and Euclidean backends can link to tools for nets and coresets. By using one simple and witness-based template for the relation between packing and covering and for search over the radius, long approximation proofs are turned into small and verifiable pieces. These pieces can be combined to build algorithms for dynamic data, streaming data, and networked systems.