Papers

2025

• [Preprint] Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust (eprint)
• [Conference] hax: Verifying Security-Critical Rust Software using Multiple Provers (VSTTE 2024, DOI: 10.1007/978-3-031-86695-1_7)
• [Preprint] hax: Verifying Security-Critical Rust Software using Multiple Provers (eprint)

2024

• [Conference] The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography (CPP-2024, DOI: 10.1145/3636501.3636961, CPP slides, Presentation or YouTube)

2023

• [Preprint] The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography (eprint)
• HACSPEC: a gateway to high-assurance cryptography (Extended abstract, RWC, YouTube, Slides)

Workshops and Seminars

• Proving the Core Security Theorem for the TLS-1.3 Key Schedule ({LogSem seminar at Aarhus University, Presentation}, {NordiCrypt-2025, Presentation})
• A formal security analysis of Blockchain voting ({CoqPL-2024 , Presentation or YouTube}, {TYPES-2024 Slides}, {ZKProof’7, Slides})
• Specifying Smart Contract with Hax and ConCert (CoqPL-2024, Presentation or YouTube)