- Andrew W. Appel, Yves Bertot. C floating-point proofs layered with VST and Flocq. J. Formalized Reasoning, 13(1):1-16, 2020.
- Andrew W. Appel, Yves Bertot. Corrigendum: C floating-point proofs layered with VST and Flocq. J. Formalized Reasoning, 13(1), 2020.
- Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto. LF+ in Coq for "fast and loose" reasoning. J. Formalized Reasoning, 12(1):11-51, 2019.
- Ranganathan Padmanabhan, Yang Zhang. Commutativity Theorems in Groups with Power-like Maps. J. Formalized Reasoning, 12(1):1-10, 2019.
- Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. J. Formalized Reasoning, 12(1):53-97, 2019.
- Reynald Affeldt, Cyril Cohen, Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formalized Reasoning, 11(1):43-76, 2018.
- César A. Muñoz, Anthony J. Narkawicz, Aaron Dutle. A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision. J. Formalized Reasoning, 11(1):19-41, 2018.
- Pierre Lescanne. Dependent Types for Extensive Games. J. Formalized Reasoning, 11(1):1-17, 2018.
- Ran Chen, Martin Clochard, Claude Marché. A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. J. Formalized Reasoning, 10(1):51-66, 2017.
- Alexander Bagnall, Samuel Merten, Gordon Stewart. A Library for Algorithmic Game Theory in Ssreflect/Coq. J. Formalized Reasoning, 10(1):67-95, 2017.