Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. - Benjamin Delaware; Clément Pit-Claudel; Jason Gross; Adam Chlipala (POPL, 2015)

Trigger Selection Strategies to Stabilize Program Verifiers. - K. Rustan M. Leino; Clément Pit-Claudel (CAV (1), 2016)

The End of History? Using a Proof Assistant to Replace Language Design with Library Design. - Adam Chlipala; Benjamin Delaware; Samuel Duchovni; Jason Gross; Clément Pit-Claudel; Sorawit Suriyakarn; Peng Wang 048; Katherine Ye (SNAPL, 2017)

Correct-by-Construction Implementation of Runtime Monitors Using Stepwise Refinement. - Teng Zhang; John Wiegley; Theophilos Giannakopoulos; Gregory Eakman; Clément Pit-Claudel; Insup Lee 001; Oleg Sokolsky (SETTA, 2018)

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. - Sorawit Suriyakarn; Clément Pit-Claudel; Benjamin Delaware; Adam Chlipala (CoRR, 2018)

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. - 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; et al. (CoRR, 2018)

Meta-F ^ star : 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; et al. (ESOP, 2019)

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. - Benjamin Delaware; Sorawit Suriyakarn; Clément Pit-Claudel; Qianchuan Ye; Adam Chlipala (Proc. ACM Program. Lang., 2019)

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. - Clément Pit-Claudel; Peng Wang 048; Benjamin Delaware; Jason Gross; Adam Chlipala (IJCAR (2), 2020)

The essence of Bluespec: a core language for rule-based hardware design. - Thomas Bourgeat; Clément Pit-Claudel; Adam Chlipala; Arvind 001 (PLDI, 2020)

Untangling mechanized proofs. - Clément Pit-Claudel (SLE, 2020)

Effective simulation and debugging for a high-level hardware language using software compilers. - Clément Pit-Claudel; Thomas Bourgeat; Stella Lau; Arvind 001; Adam Chlipala (ASPLOS, 2021)

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. - Clément Pit-Claudel; Jade Philipoom; Dustin Jamner; Andres Erbsen; Adam Chlipala (PLDI, 2022)

Relational compilation: Functional-to-imperative code generation for performance-critical applications. - Clément Pit-Claudel (2022)

Specification and Verification of Strong Timing Isolation of Hardware Enclaves. - Stella Lau; Thomas Bourgeat; Clément Pit-Claudel; Adam Chlipala (CCS, 2024)

Practical Verification of System-Software Components Written in Standard C. - Can Cebeci; Yong-Hao Zou; Diyu Zhou; George Candea; Clément Pit-Claudel (SOSP, 2024)

Incremental Proof Development in Dafny with Module-Based Induction. - Son Ho; Clément Pit-Claudel (CoRR, 2024)

Linear Matching of JavaScript Regular Expressions. - Aurèle Barrière; Clément Pit-Claudel (Proc. ACM Program. Lang., 2024)

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types. - Aleksander Boruch-Gruszecki; Adrien Ghosn; Mathias Payer; Clément Pit-Claudel (Proc. ACM Program. Lang., 2024)

Foundational Integration Verification of a Cryptographic Server. - Andres Erbsen; Jade Philipoom; Dustin Jamner; Ashley Lin; Samuel Gruetter; Clément Pit-Claudel; Adam Chlipala (Proc. ACM Program. Lang., 2024)

A Coq Mechanization of JavaScript Regular Expression Semantics. - Noé De Santo; Aurèle Barrière; Clément Pit-Claudel (Proc. ACM Program. Lang., 2024)

Verified and Optimized Implementation of Orthologic Proof Search. - Simon Guilloud; Clément Pit-Claudel (CAV (3), 2025)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications. - Aurèle Barrière; Victor Deng; Clément Pit-Claudel (CoRR, 2025)