Research internships | Key projects | Education | Teaching | Professional experiences | Contact
I'm a student in the second year of Parisian Master of Research in Computer Science (MPRI), at École Normale Supérieure Paris-Saclay (ENS Paris-Saclay).
My research interests include formal methods, program verification and software engineering, particularly in the verification of real-world programs using separation logic and automated theorem proving.
Under the supervision of
Derek Dreyer and
Lennard Gäher.
From October 2023 to June 2024 (9 months) – MPI-SWS, Saarbrücken, Germany.
Rust, a modern systems programming language, has recently gained attention due to its promises on memory safety. Consequently, there has been significant research into building verification tools capable of stablishing functional correctness properties of Rust programs.
One such endeavor is RefinedRust, a recent initiative focused on automating end-to-end verification, offering high assurances through the generation of foundational proofs within the Rocq proof assistant and the Iris separation logic framework.
A distinguishing feature of RefinedRust lies in its capability to not only verify safe Rust programs but also extend support for reasoning about unsafe code, a crucial component in Rust’s ecosystem for writing programs where Rust cannot statically certify memory safety. Notably, it is widely used within the implementation of Rust’s standard library.
This internship extends RefinedRust by integrating support for reasoning about interior mutability, enabling its use for proving specifications about types, like Cell.
See the report See the slides See the poster
Under the supervision of
Lars Birkedal and
June Rousseau.
From February 2023 to July 2023 (6 months) – Aarhus University, Denmark.
A capability machine is a type of CPU that uses capabilities, enriched pointers used to prevent unauthorised access to memory. Using seals, capabilities can be locked to prevent any use until unlocked, thus ensuring authenticity.
This mechanism has recently been added to Cerise, a framework to reason on interaction of known and unknown code. This internship provides an explanation of seals and a new example of how to implement a global mutable store using seals.
See the report See the slides
Under the supervision of
Frédéric Besson.
From June to July 2022 (7 weeks) – IRISA Rennes, France.
The Linux kernel executes operations in privileged mode without the guarantees offered by user space. As a result, any memory corruption in the kernel can have serious security consequences. However, it is sometimes desirable to allow users to extend the kernel's functionality with external programs.
The alternative currently implemented in the Linux kernel is eBPF (Extended Berkeley Packet Filter), based on the principles of BPF. eBPF makes it possible to obtain secure and rapid extensions to the kernel using a static verifier and on-the-fly compilation. eBPF technology has gained interest in the RIOT microkernel, which is specifically designed for microcontrollers. However, eBPF's design choices are not suitable for these machines. eBPF has a 64-bit instruction set and microcontrollers are 32-bit machines.
This internship adds and proves the correctness of a backend, called rBPF, to the CompCert certified compiler, which generates optimised code that respects the constraints of the microcontrollers.
See the report (in French) See the slides (in French)Join work with Arthur Adjedj, Augustin Albert and Lucas Tabary-Maujean.
This project aims to provide a small tool for type checking expressions written in the language of the Calculus of Construction (CoC).
Extra care has been taken to design an efficient memory management model that uses a common memory location for lambda-terms. This ensures invariants like unicity of a term in memory which provides laziness and allowing the results of the most expensive functions to be stored (memoising).
From a developer's perspective, this memory model provides stronger isolation properties, preventing several memory pools from interacting with each other, allowing independent parallel execution.
See the repositoryThis project aims to provide a close interoperability between Scala (in its LLVM form, called Scala Native) and C++ languages, both being object-oriented languages.
The main point is to make Scala omniscient over the binary interface of C++, where the latter is unchanged. As such, a library in C++ can be used directly in Scala without modifing the C++ code nor the C++ compiled library.
Moreover, Scala being garbage-collected and C++ being explicitly managed, interesting questions about memory management have arisen.
Notably, an instance of this research is used as the main dependency of a programming project for bachelor students at École Normale Supérieure Paris-Saclay.
See the repositoryFrom 2021 to 2025 (4 years), Gif-sur-Yvette, France.
Learning through theoretical pedagogy to study the field of formal methods. I am studying the mechanisms of the OCaml and Rust languages, as well as the Coq proof assistant.
From 2019 to 2021 (2 years), Bordeaux, France.
Theoretical discovery of computer science, coupled with learning mathematics. I studied algorithms in various fields using the C and OCaml languages.
From 2017 to 2020 (3 years), Bordeaux, France.
Practical discovery of informatics through group projects. I experimented with many programming languages through systems programming.
Under the supervision of Burkhart Wolff.
From September 2022 to December 2022 (48h) – Université Paris-Saclay, France.
Teaching formal methods as teaching assistant to third year students.
From September 2020 to March 2022 (189h), Epitech Bordeaux, France.
Teaching applied mathematics (B-MAT-100 to B-MAT-500) and UNIX systems programming (B-PSU-402) to first to third year students as the main teacher.
Done remotely due to covid lockdown, and realised using chroma key setup.
Under the supervision of Benjamin Barrois.
From March to June 2020 (4 months), Hiventive, Bordeaux, France.
Improvement and development of microservices of a CAPE project.
Under the supervision of Jérôme Maury.
From May to August 2019 (4 months), Normad1, Bordeaux, France.
Implementation of a multi-platform network stack.
Under the supervision of Jérôme Maury.
From July to December 2018 (6 months), Normad1, Bordeaux, France.
Verification of a code base using fuzzing based methods.
You can reach me by email: <firstname> [dot] <lastname> [at] proton.me.
My PGP key is available here: ignore any email that has not been signed with it.
You can find my projects on my Codeberg profile.
You can also find me outside contributing to OpenStreetMap.
Last updated: 28th february 2025