La verificación formal de la teoría matemática ha recibido una amplia atención y ha crecido rápidamente. La formalización de la teoría fundamental contribuirá al desarrollo de grandes proyectos. En este documento, presentamos la formalización en Coq del cálculo sin teoría de límites. La teoría tiene como objetivo establecer una nueva forma de cálculo más fácil pero rigurosa. Esta teoría, como innovación, difiere del cálculo tradicional pero es equivalente y más comprensible. Primero, se da de manera intuitiva la definición de la función de control del cociente diferencial a partir de los hechos físicos. Luego, se le añaden condiciones para obtener la derivada y se define la integral mediante la axiomatización. Posteriormente, algunas conclusiones importantes en cálculo como la fórmula de Newton-Leibniz y la fórmula de Taylor pueden ser verificadas formalmente. Esto demuestra que esta teoría puede ser independiente de la teoría de límites y que ninguna prueba implica la completitud de los números reales. Este trabajo puede ayudar a los estudiantes a estudiar cálculo y sentar las bases para muchas aplicaciones.