A formalisation of LEGv8 in Agda. - Santiago Arranz-Olmos; Martín Fernández; Matías Steinberg; Alejandro Gadea; Emmanuel Gunther; Miguel Pagano (SBLP, 2020)

Transitive Models of Fragments of ZFC. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf; Matías Steinberg (Arch. Formal Proofs, 2022)

The Independence of the Continuum Hypothesis in Isabelle/ZF. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf; Matías Steinberg (Arch. Formal Proofs, 2022)

The formal verification of the ctm approach to forcing. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf; Matías Steinberg (Ann. Pure Appl. Log., 2024)