Introduction to Formal Methods Using Interactive Proof Assistant Rocq

Evgeny Makarov

Abstract


This article describes our experience of introducing undergraduate students to formal methods using the interactive proof assistant Rocq. The goals of the course include sharpening students' skills in writing strict mathematical proofs both on paper and on a computer, as well as demonstrating practical applications of mathematical logic. At the end of the course students do group projects where they specify and verify an algorithm, such as finding maximum in a one- or two-dimensional array, checking if a number is prime or computing an integer root of an equation.
We tried to minimize nontrivial aspects of Rocq and use the most of the material already familiar to students. This comparative simplicity, which is appropriate for the first introduction to formal methods, distinguishes the course from its analogs.

Full Text:

PDF

References


E. Makarov. (2025). Algorithm verification using the interactive theorem prover Rocq, [Online]. Available: https://evgenymakarov.github.io/unnfcs2019/.

E. M. Clarke and J. M. Wing, “Formal methods: State of the art and future directions,” ACM Comput. Surv., vol. 28, no. 4, pp. 626–643, 1996. DOI: 10.1145/242223.242257.

E. Feron, “Formal methods for aerospace applications,” in Formal Methods in Computer-Aided Design. FMCAD 2012, IEEE, 2012, p. 3.

W. A. Hunt Jr., M. Kaufmann, J. S. Moore, and A. Slobodova, “Industrial hardware and software verification with ACL2,” Philos Trans A Math Phys Eng Sci., vol. 375, no. 2104, 2017. DOI: 10.1098/rsta.2015.0399.

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon web services uses formal methods,” Commun. ACM, vol. 58, no. 4, pp. 66–73, 2015. DOI: 10.1145/2699417.

F. Wiedijk, The Seventeen Provers of the World, ser. Lecture Notes in Artificial Intelligence. Berlin, Heidelberg: Springer-Verlag, 2006, vol. 3600. DOI: 10.1007/11542384.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, ser. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. DOI: 10.1007/978-3-662-07964-5.

The Rocq Development Team, The Rocq Reference Manual, version 9.0.0. INRIA, 2025. [Online]. Available: https://rocq-prover.org/doc/V9.0.0/refman/index.html.

E. Makarov and B. Spitters, “The Picard algorithm for ordinary differential equations in Coq,” in Interactive Theorem Proving. ITP 2013, S. Blazy, C. Paulin-Mohring, and D. Pichardie, Eds., ser. Lecture Notes in Computer Science, vol. 7998, Springer, 2013, pp. 463–468. DOI: 10.1007/978-3-642-39634-2_34.

G. Gonthier, “Formal proof—the four-color theorem,” Notices Amer. Math. Soc., vol. 55, no. 11, pp. 1382–1393, 2008.

R. O’Connor, “Essential incompleteness of arithmetic verified by Coq,” in Theorem Proving in Higher Order Logics. TPHOLs 2005, J. Hurd and T. Melham, Eds., ser. Lecture Notes in Computer Science, vol. 3603, Springer, 2005, pp. 245–260. DOI: 10.1007/ 11541868_16.

G. Gonthier et al., “Machine-checked proof of the odd order theorem,” in 4th Conference on Interactive Theorem Proving, TP 2013, ser. Lecture Notes in Computer Science, vol. 7998, 2013, pp. 163–179. DOI: 10.1007/978-3-642-39634-2_14.

R. Krebbers, X. Leroy, and F. Wiedijk, “Formal C semantics: CompCert and the C standard,” in Interactive Theorem Proving. ITP 2014, G. Klein and R. Gamboa, Eds., ser. Lecture Notes in Computer Science, vol. 8558, Springer, 2014, pp. 543–548. DOI: 10.1007/978-3-319-08970-6_36.

B. C. Pierce et al., Software Foundations. Electronic textbook, 2025. [Online]. Available: https://softwarefoundations.cis.upenn.edu/.

B. Russell, Introduction to Mathematical Philosophy. Dover Publications, 1993.

M. Hendriks, C. Kaliszyk, F. van Raamsdonk, and F. Wiedijk, “Teaching logic using a state-of-the-art proof assistant,” Acta Didactica Napocensia, vol. 3, no. 2, pp. 35–48, 2010.

M. Henz and A. Hobor, “Teaching experience: Logic and formal methods with Coq,” in Certified Programs and Proofs, J.-P. Jouannaud and Z. Shao, Eds., Springer, 2011, pp.199–215. DOI: 10.1007/978-3-642-25379-9_16.

S. Böhne and C. Kreitz, “Learning how to prove: From the Coq proof assistant to textbook style,” in Proceedings 6th International Workshop on Theorem Proving Components for Educational Software, P. Quaresma and W. Neuper, Eds., ser. Electronic Proceedings in Theoretical Computer Science, vol. 267, Open Publishing Association, 2018, pp. 1–18. DOI: 10.4204/EPTCS.267.1.

T. M. Pham and Y. Bertot, “A combination of a dynamic geometry software with a proof assistant for interactive formal proofs,” Electronic Notes in Theoretical Computer Science,vol.285,pp.43–55, 2012. DOI: 10.1016/j.entcs.2012.06.005.

T. Nipkow, “Teaching semantics with a proof assistant: No more LSD trip proofs,” in Verification, Model Checking, and Abstract Interpretation. VMCAI 2012, V. Kuncak and A. Rybalchenko, Eds., ser. Lecture Notes in Computer Science, vol. 7148, 2012, pp. 24–38. DOI: 10.1007/978-3-642-27940-9_3.

J.-C. Filliâtre and A. Paskevich, “Why3 — where programs meet provers,” in Proceedings of the 22nd European Symposium on Programming, M. Felleisen and P. Gardner, Eds., ser. Lecture Notes in Computer Science, vol. 7792, Springer, Mar. 2013, pp. 125–128. [Online]. Available: https://hal.inria.fr/hal-00789533.


Refbacks

  • There are currently no refbacks.


Abava  Кибербезопасность ИТ конгресс СНЭ

ISSN: 2307-8162