Foundational Research with F*

The Design of F* and its DSLs

Programming and Proving with Indexed Effects

Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro and Nikhil Swamy.

Technical report, 2021.

Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic

Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux and Tahina Ramananandro.

25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021.

A Verified, Efficient Embedding of a Verifiable Assembly Language

Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi and Nikhil Swamy.

PACMPL, no. POPL, 2019.

Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi and Nikhil Swamy.

28th European Symposium on Programming (ESOP), pp. 30–59, 2019.

Verified Low-Level Programming Embedded in F*

Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet and Nikhil Swamy.

PACMPL, vol. 1, no. ICFP, pp. 17:1–17:29, 2017.

Dependent Types and Multi-Monadic Effects in F*

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué and Santiago Zanella-Béguelin.

43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 256–270, 2016.

Semantics and Effects

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs

Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro and Nikhil Swamy.

Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, article 208, 25 pages, 2025.

SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs

Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman and Guido Martínez.

25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2020.

Dijkstra Monads for All

Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas and Éric Tanter.

24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019.

The Next 700 Relational Program Logics

Kenji Maillard, Catalin Hritcu, Exequiel Rivas and Antoine Van Muylder.

arXiv:1907.05244, 2019.

A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations

Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy and Santiago Zanella-Béguelin.

The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018.

Recalling a Witness: Foundations and Applications of Monotonic State

Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi and Nikhil Swamy.

PACMPL, vol. 2, no. POPL, pp. 65:1–65:30, 2018.

Dijkstra Monads for Free

Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi and Nikhil Swamy.

44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 515–529, 2017.

Towards a Provably Correct Encoding from F* to SMT

Alejandro Aguirre.

Inria Internship Report, 2016.

Verifying Higher-order Programs with the Dijkstra Monad

Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen and Benjamin Livshits.

Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, pp. 387–398, 2013.

USSL: A Universe-Stratified Concurrent Separation Logic for Intrinsic Proofs of Dependently Typed Programs

Anonymous authors.

Undated preprint.

Applications in Security and Cryptography

DY* Unchained: Now with Composable Security Proofs and Precise Compromise Scenarios

Théophile Wallez.

2026 IEEE Symposium on Security and Privacy (SP), pp. 1–18, 2026.

Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software

Danel Ahman, Karthikeyan Bhargavan, Barry Bond, Jay Bosamiya, Christopher Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hrițcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy and Santiago Zanella-Béguelin.

ACM Transactions on Programming Languages and Systems, vol. 48, no. 2, article 9, pp. 9:1–9:64, 2026.

Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust

Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch and Bas Spitters.

Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, pp. 2729–2743, 2025.

Comparse: Provably Secure Formats for Cryptographic Protocols

Wallez, Théophile, Protzenko, Jonathan and Bhargavan, Karthikeyan.

Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, pp. 564–578, 2023.

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification

Ho, Son, Fromherz, Aymeric and Protzenko, Jonathan.

Proc. ACM Program. Lang., vol. 7, no. ICFP, article 202, 32 pages, 2023.

TreeSync: Authenticated Group Management for Messaging Layer Security

Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche and Karthikeyan Bhargavan.

Proceedings of the 32th USENIX Conference on Security Symposium, 2023.

Verifying Indistinguishability of Privacy-Preserving Protocols

Linvill, Kirby, Kaki, Gowtham and Wustrow, Eric.

Proc. ACM Program. Lang., vol. 7, no. OOPSLA2, article 273, 28 pages, 2023.

Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations

Ho, Son, Protzenko, Jonathan, Bichhawat, Abhishek and Bhargavan, Karthikeyan.

2022 IEEE Symposium on Security and Privacy (SP), pp. 107–124, 2022.

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer

Delignat-Lavaud, Antoine, Fournet, Cédric, Parno, Bryan, Protzenko, Jonathan, Ramananandro, Tahina, Bosamiya, Jay, Lallemand, Joseph, Rakotonirina, Itsaka and Zhou, Yi.

2021 IEEE Symposium on Security and Privacy (SP), pp. 1162–1178, 2021.

A Tutorial-Style Introduction to DY*

Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim.

Protocols, Strands, and Logic: Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday, pp. 77–97, 2021.

An In-Depth Symbolic Security Analysis of the ACME Standard

Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim.

Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, pp. 2601–2617, 2021.

DICE*: A Formally Verified Implementation of DICE Measured Boot

Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani and Aditya V. Thakur.

30th Usenix Security Symposium, 2021.

DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code

Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim.

2021 IEEE European Symposium on Security and Privacy (EuroS&P), pp. 523–542, 2021.

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider

Protzenko, Jonathan, Parno, Bryan, Fromherz, Aymeric, Hawblitzel, Chris, Polubelova, Marina, Bhargavan, Karthikeyan, Beurdouche, Benjamin, Choi, Joonwon, Delignat-Lavaud, Antoine, Fournet, Cédric, Kulatova, Natalia, Ramananandro, Tahina, Rastogi, Aseem, Swamy, Nikhil, Wintersteiger, Christoph M. and Zanella-Beguelin, Santiago.

2020 IEEE Symposium on Security and Privacy (SP), pp. 983–1002, 2020.

HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms)

Polubelova, Marina, Bhargavan, Karthikeyan, Protzenko, Jonathan, Beurdouche, Benjamin, Fromherz, Aymeric, Kulatova, Natalia and Zanella-Béguelin, Santiago.

Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, pp. 899–918, 2020.

Formally Verified Cryptographic Web Applications in WebAssembly

J. Protzenko, B. Beurdouche, D. Merigoux and K. Bhargavan.

2019 IEEE Symposium on Security and Privacy (SP), 2019.

Wys*: A DSL for Verified Secure Multi-party Computations

Aseem Rastogi, Nikhil Swamy and Michael Hicks.

8th International Conference on Principles of Security and Trust (POST), vol. 11426, pp. 99–122, 2019.

Everest: Towards a Verified, Drop-in Replacement of HTTPS

Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin and Jean-Karim Zinzindohoué.

2nd Summit on Advances in Programming Languages, 2017.

HACL*: A Verified Modern Cryptographic Library

Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko and Benjamin Beurdouche.

ACM Conference on Computer and Communications Security, pp. 1789–1806, 2017.

Implementing and Proving the TLS 1.3 Record Layer

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin and Jean Karim Zinzindohoue.

IEEE Security & Privacy, 2017.

Applications in Systems

Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic

Guido Martínez, Bastian Köpcke, Jonáš Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer, Tyler Sorensen and Nikhil Swamy.

Proceedings of the ACM on Programming Languages, vol. 10, no. PLDI, pp. 830–854, 2026.

Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems

Amos Robinson and Alex Potanin.

38th European Conference on Object-Oriented Programming, ECOOP 2024, September 16-20, 2024, Vienna, Austria, vol. 313, pp. 34:1–34:28, 2024.

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

Antonin Reitz, Aymeric Fromherz and Jonathan Protzenko.

CoRR, vol. abs/2403.09435, 2024.

FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores

Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno and Ravi Ramamurthy.

Certified Programs and Proofs, 2023.

Provably-Safe Multilingual Software Sandboxing using WebAssembly

Bosamiya, Jay, Lim, Wen Shih and Parno, Bryan.

Proceedings of the USENIX Security Symposium, 2022.

FastVer: Making Data Integrity a Commodity

Arasu, Arvind, Chandramouli, Badrish, Gehrke, Johannes, Ghosh, Esha, Kossmann, Donald, Protzenko, Jonathan, Ramamurthy, Ravi, Ramananandro, Tahina, Rastogi, Aseem, Setty, Srinath, Swamy, Nikhil, van Renen, Alexander and Xu, Min.

Proceedings of the 2021 International Conference on Management of Data, pp. 89–101, 2021.

Applications in Parsing

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

Tahina Ramananandro, Gabriel Ebner, Guido Martínez and Nikhil Swamy.

Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, pp. 2744–2758, 2025.

ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER

Ni, Haobin, Delignat-Lavaud, Antoine, Fournet, Cédric, Ramananandro, Tahina and Swamy, Nikhil.

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 275–289, 2023.

Hardening Attack Surfaces with Formally Proven Binary Format Parsers

Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona and Arti Gupta.

Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '22), June 13–17, 2022, San Diego, CA, USA, 2022.

Everparse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats

Ramananandro, Tahina, Delignat-Lavaud, Antoine, Fournet, Cédric, Swamy, Nikhil, Chajed, Tej, Kobeissi, Nadim and Protzenko, Jonathan.

Proceedings of the 28th USENIX Conference on Security Symposium, pp. 1465–1482, 2019.

Applications in Programming, Program Proof, and Program Analysis

Misquoted No More: Securely Extracting F* Programs with IO

Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas and Théo Winterhalter.

Proceedings of the ACM on Programming Languages, vol. 10, no. ICFP, pp. 494–523, 2026.

A Mechanically Verified Garbage Collector for OCaml

Sheera Shamsu, Dipesh Kafle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan and KC Sivaramakrishnan.

Journal of Automated Reasoning, vol. 69, no. 2, article 11, 2025.

Automatically Verifying Replication-Aware Linearizability

Vimala Soundarapandian, Kartik Nagar, Aseem Rastogi and KC Sivaramakrishnan.

Proceedings of the ACM on Programming Languages, vol. 9, no. OOPSLA1, pp. 871–897, 2025.

SecRef: Securely Sharing Mutable References between Verified and Unverified Code in F

Andrici, Cezar-Constantin, Ahman, Danel, Hri\ctcu, C\uat\ualin, Icleanu, Ruxandra, Martínez, Guido, Rivas, Exequiel and Winterhalter, Théo.

Proc. ACM Program. Lang., vol. 9, no. ICFP, article 253, 31 pages, 2025.

Securing Verified IO Programs Against Unverified Code in F*

Andrici, Cezar-Constantin, Ciobâcă, Ștefan, Hri\ctcu, C\uat\ualin, Martínez, Guido, Rivas, Exequiel, Tanter, Éric and Winterhalter, Théo.

Proc. ACM Program. Lang., vol. 8, no. POPL, article 74, 34 pages, 2024.

Pipit: Reactive Systems in F* (Extended Abstract)

Amos Robinson and Alex Potanin.

TyDe 2023 (extended abstract), 2023.

Aeneas: Rust Verification by Functional Translation

Ho, Son and Protzenko, Jonathan.

Proc. ACM Program. Lang., vol. 6, no. ICFP, article 116, 31 pages, 2022.

Certified Mergeable Replicated Data Types

Soundarapandian, Vimala, Kamath, Adharsh, Nagar, Kartik and Sivaramakrishnan, KC.

Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 332–347, 2022.

Q: Implementing Quantum Separation Logic in F

Kesha Hietala, Sarah Marshall, Robert Rand and Nikhil Swamy.

PLanQC 2022 (extended abstract), 2022.

Catala: A Programming Language for the Law

Merigoux, Denis, Chataing, Nicolas and Protzenko, Jonathan.

Proc. ACM Program. Lang., vol. 5, no. ICFP, article 77, 29 pages, 2021.

Verification of a Merkle Patricia Tree Library Using F*

Sota Sato, Ryotaro Banno, Junji Furuse, Kohei Suenaga and Atsushi Igarashi.

ArXiv, vol. abs/2106.04826, 2021.

Verified Functional Programming of an Abstract Interpreter

Franceschino, Lucas, Pichardie, David and Talpin, Jean-Pierre.

Static Analysis, pp. 124–143, 2021.

Statically Verified Refinements for Multiparty Protocols

Zhou, Fangyi, Ferreira, Francisco, Hu, Raymond, Neykova, Rumyana and Yoshida, Nobuko.

Proc. ACM Program. Lang., vol. 4, no. OOPSLA, article 148, 30 pages, 2020.

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language

Bosamiya, Jay, Gibson, Sydney, Li, Yao, Parno, Bryan and Hawblitzel, Chris.

Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020.

Verified Compilation of Space-Efficient Reversible Circuits

Amy, Matthew, Roetteler, Martin and Svore, Krysta M..

Computer Aided Verification, pp. 3–21, 2017.

AI-assisted Programming

Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)

Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose and Tahina Ramananandro.

Proceedings of the ACM on Programming Languages, vol. 10, no. ICFP, pp. 1059–1077, 2026.

The ART of Agentic Proof-Oriented Programming: Audits, Rubrics, and Templates

Nikhil Swamy, Tahina Ramananandro, Guido Martínez, Gabriel Ebner, Shuvendu Lahiri and Lef Ioannidis.

Preprint, 2026.

3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers

Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro and Nikhil Swamy.

2024.

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri and Nikhil Swamy.

CoRR, vol. abs/2405.01787, 2024.

Miscellaneous

A Theorem Proving Approach to Programming Language Semantics

Subhajit Roy.

2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering Education and Training (ICSE-SEET), pp. 153–165, 2023.

Foundational Research with F*

The Design of F* and its DSLs

Semantics and Effects

Applications in Security and Cryptography

Applications in Systems

Applications in Parsing

Applications in Programming, Program Proof, and Program Analysis

AI-assisted Programming

Miscellaneous

Papers about an older version of F*