We have built formally verified numerical methods components (see verinum.org) such as linear solvers (by Jacobi iteration or Cholesky decomposition), Lagrange shape functions, Gaussian quadrature, dense and sparse matrix representations (compressed sparse row, banded matrices) and operations on them (construction, matrix multiply, Cholesky). In Rocq we prove theorems about these algorithms in the real numbers, we prove accuracy theorems relating those to the corresponding algorithms in IEEE floating point, and we prove that C programs correctly and exactly implement those floating-point algorithms. We use accurate and detailed formalizations of IEEE floating point and of the operational semantics (and memory model) of the C programming language. The results are end-to-end machine-checked (Rocq) theorems of the correctness and accuracy of numerical methods implemented in C, with respect to the high-level mathematical problems they are intended to solve. We are working towards a verification of a Finite Element Method solver, which includes all the above-mentioned components plus a few more (such as mesh topology, mesh geometry, relation of reference domain to spatial domain) that we have yet to do. This is joint work with David Bindel, Jean-Baptiste Jeannin, and others.