Consultant at Tweag/Modus Create. I joined Tweag in September 2021, which was then acquired by Modus Create in June 2022. Tweag/Modus Create is a consultancy specialised, as far as I am concerned, in functional languages (most notably OCaml and Haskell) and Nix/NixOS. I have, since I joined, worked in very different contexts, with very different people, on very different projects. In addition to client work, I am a squad lead internally, mentoring fellow engineers as well as following them and communicating on their behalf to other instances of the company.

Nix engineer at Tweag/Modus Create. In September 2024, I joined the Nix team at Tweag and started working on the Fediversity project. This project, supported by NLnet, consists on my part in the development of NixOS modules, NixOS tests, and NixOps4 providers and resources to ease the deployment of clusters of machines serving Fediverse software, among other things, to thousands of users.

Haskell architect at Tweag/Modus Create. From January to March 2025, with a team of Haskell engineers from Modus Create, we looked into an enhancement to the consensus algorithm of the Cardano blockchain, called Ouroboros Peras (not to be confused with my work on Ouroboros Genesis from July 2023 to July 2024). We analysed feasability and gave recommendations on how this new functionality should be implemented.

Software auditor at Tweag/Modus Create. From August to October 2024, I ran code audit for codebases in OCaml or Haskell. Those varied drastically in scope, but some have been security audits for web applications, in which case I was paired with a security auditor of Modus Create. I then stopped this activity to focus entirely on Fediversity.

Haskell engineer at Tweag/Modus Create. From July 2023, with a team of Haskell engineers from Modus Create, we enhanced the consensus algorithm of the Cardano blockchain, creating tooling to run richer and more complex tests than what existed before, and addressing the vulnerabilities of nodes joining or rejoining the network. This effort terminated during the summer 2024 and the new algorithm, going by the sweet name of Ouroboros Genesis, is in the process of being deployed in Cardano nodes.

Research software engineer at Tweag/Modus Create. Following my work with Hachi, I joined the internal High Assurance Software group in September 2022, where I worked towards a similar purpose on a different tool suite written in Haskell: I helped develop Pirouette and Cooked Validators.

Research software engineer at Tweag/Modus Create. In September 2021, shortly after starting my work at Tweag, I joined Hachi, an R+D effort by MELD aiming at building a dynamic analysis tool suite for smart contracts on Cardano, mostly in Racket. I was mostly working on the concolic execution of smart contracts and on a DSL to specify expectations of such contracts. The effort was discontinued in August 2022.

PhD in computer science at IRIF (Université de Paris, France) with Ralf Treinen and Yann Régis-Gianas on the “Verification of Shell Scripts Performing File Hierarchy Transformations”. This involved a more theoretical side working on extending feature tree logics and working on their decidability; and a more practical side implementing the actual analysis tooling, from a parser of Shell to a satisfiability solver for formulas in our logics. This effort led to the report of over 150 bugs on Debian packages.

ENS graduate degree at the École normale supérieure (Paris, France). This is a research-oriented four-year program including the third year of bachelor, the two years of master and an extra year — in my case, a one year-long internship. The degree requires the validation of extra courses in addition to the bachelor and master.

Master's degree in computer science at the Université de Paris (France). The “Master Parisien de Recherche en Informatique” is a research-oriented master program in computer science whose purpose is to train future scientists through intensive exposure to contemporary research.

See more about my professional experience, my education or my PhD thesis.

I like specifications, abstraction and modularisation. I firmly believe in strongly typed functional programming, compilers, formal methods and program verification.

I enjoy working on low-level objects — network, systems or code optimisation, for instance. I am not afraid to dig into standards and RFCs.

I try to write good code, well designed and documented, used in practice.

On my free time, I administrate a Debian server providing websites, email, cloud, etc.

I love teaching and giving talks and I am said to be good at it.

OCaml, POSIX Shell

Fluent in French and English

Haskell, Racket, TeX/LaTeX

Web, C, Java, Python, other Lisp

I spend a lot of time playing music (piano & clarinet mostly, but I love trying all kind of instruments), writing music and typesetting music (with LilyPond).

I also spend an awful lot of time doing Scottish Country Dancing. This includes dancing it, teaching it, playing music for it and organising local and international events.

Consultant at Tweag/Modus Create. I joined Tweag in September 2021, which was then acquired by Modus Create in June 2022. Tweag/Modus Create is a consultancy specialised, as far as I am concerned, in functional languages (most notably OCaml and Haskell) and Nix/NixOS. I have, since I joined, worked in very different contexts, with very different people, on very different projects. In addition to client work, I am a squad lead internally, mentoring fellow engineers as well as following them and communicating on their behalf to other instances of the company.

Nix engineer at Tweag/Modus Create. In September 2024, I joined the Nix team at Tweag and started working on the Fediversity project. This project, supported by NLnet, consists on my part in the development of NixOS modules, NixOS tests, and NixOps4 providers and resources to ease the deployment of clusters of machines serving Fediverse software, among other things, to thousands of users.

Haskell architect at Tweag/Modus Create. From January to March 2025, with a team of Haskell engineers from Modus Create, we looked into an enhancement to the consensus algorithm of the Cardano blockchain, called Ouroboros Peras (not to be confused with my work on Ouroboros Genesis from July 2023 to July 2024). We analysed feasability and gave recommendations on how this new functionality should be implemented.

Software auditor at Tweag/Modus Create. From August to October 2024, I ran code audit for codebases in OCaml or Haskell. Those varied drastically in scope, but some have been security audits for web applications, in which case I was paired with a security auditor of Modus Create. I then stopped this activity to focus entirely on Fediversity.

Haskell engineer at Tweag/Modus Create. From July 2023, with a team of Haskell engineers from Modus Create, we enhanced the consensus algorithm of the Cardano blockchain, creating tooling to run richer and more complex tests than what existed before, and addressing the vulnerabilities of nodes joining or rejoining the network. This effort terminated during the summer 2024 and the new algorithm, going by the sweet name of Ouroboros Genesis, is in the process of being deployed in Cardano nodes.

Research software engineer at Tweag/Modus Create. Following my work with Hachi, I joined the internal High Assurance Software group in September 2022, where I worked towards a similar purpose on a different tool suite written in Haskell: I helped develop Pirouette and Cooked Validators.

Research software engineer at Tweag/Modus Create. In September 2021, shortly after starting my work at Tweag, I joined Hachi, an R+D effort by MELD aiming at building a dynamic analysis tool suite for smart contracts on Cardano, mostly in Racket. I was mostly working on the concolic execution of smart contracts and on a DSL to specify expectations of such contracts. The effort was discontinued in August 2022.

Member of the organising committee of CONFLANG, a workshop colocated with SPLASH in October 2021.

PhD in computer science at IRIF (Université de Paris, France) with Ralf Treinen and Yann Régis-Gianas on the “Verification of Shell Scripts Performing File Hierarchy Transformations”. This involved a more theoretical side working on extending feature tree logics and working on their decidability; and a more practical side implementing the actual analysis tooling, from a parser of Shell to a satisfiability solver for formulas in our logics. This effort led to the report of over 150 bugs on Debian packages.

Teaching at UFR Informatique (Université de Paris, France) including both practical and written exercises sessions for a total of 240h over 4 years. In addition to these hours in front of the students, the work included preparing materials and grading exams and projects.

Google Summer of Code with Aymeric Fromherz and Nikos Gorogiannis: “Verification and Testing of Heap-based Programs with Symbolic PathFinder”.

Research internship at IRIF (Université de Paris, France) with Ralf Treinen and Mihaela Sighireanu: “Correctness of Linux Scripts”.

Research internship at IRIF (Université de Paris, France) with Ralf Treinen and Mihaela Sighireanu: “Towards Verification of Shell Scripts”.

Research internship in the Complogic team (McGill University, Montréal, Canada) with Brigitte Pientka in order to help with the development of the proof assistant Beluga.

Research internship at the Institut de Mathématiques de Marseille (France) with Lionel Vaulx Auclair and Emmanuel Beffara: “On a logical counterpart of local non-determinism in classical realisability”.

ENS graduate degree at the École normale supérieure (Paris, France). This is a research-oriented four-year program including the third year of bachelor, the two years of master and an extra year — in my case, a one year-long internship. The degree requires the validation of extra courses in addition to the bachelor and master.

Master's degree in computer science at the Université de Paris (France). The “Master Parisien de Recherche en Informatique” is a research-oriented master program in computer science whose purpose is to train future scientists through intensive exposure to contemporary research.

Bachelor's degree in computer science at the École normale supérieure (Paris, France). The two years of preparatory classes, completed by first year of the École normale supérieure, include a full bachelor.

Preparatory classes MPSI/MP* at the Lycée du Parc (Lyon, France). Preparatory classes are an intensive two-year preparation for competitive entrance into top engineering and research schools.

President of the RSCDS Paris Branch. I lead the organising committee and represent the branch in front of the members, the RSCDS and the other branches.

Teacher of Scottish country dance classes at the RSCDS Paris Branch.

Musician for Scottish country dance classes at the RSCDS Paris Branch and internationally.

Editor of the Paris Book of Scottish Country Dances, volume 2 (2021) and volume 3 (2024) as well as their companion books of tunes. This involves communicating with the different authors, handling copyright considerations, typesetting the book (using LaTeX and LilyPond), printing and publishing it, etc.

Member of the organising committee of the RSCDS Paris Branch.

Organiser and member of a professional band (~2-3 musicians) playing at various events, mostly weddings. This includes finding the gigs, discussing the organisation with the clients and, of course, playing music.

Organiser and member of an amateur band (~10-12 musicians) playing for Scottish country dances.

Student volunteer at POPL in Paris, France.

Sanitation worker for the city of Mions, France.

Member of the organising committee of the Orchestre d’Harmonie de Saint-Priest, an amateur wind orchestra, and its associated music school, Vive le Vent.

“Verification of Shell Scripts Performing File Hierarchy Transformations”. Nicolas Jeannerod. PhD Thesis. PDF (not the final version). Dedicated Page.

“Analysing installation scenarios of Debian packages”. Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu and Ralf Treinen. In TACAS 2020 – 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Core Ranking 2020: A. Article.

“Morbig: A Static parser for POSIX shell”. Yann Régis-Gianas, Nicolas Jeannerod and Ralf Treinen. In Journal of Computer Languages, Volume 57, April 2020. Article.

“Morbig: A Static Parser for POSIX Shell”. Yann Régis-Gianas, Nicolas Jeannerod and Ralf Treinen. In SLE 2018 - 11th International Conference on Software Language Engineering. Core Ranking 2018: B. Article.

“Deciding the First-Order Theory of an Algebra of Feature Trees with Updates”. Nicolas Jeannerod and Ralf Treinen. In IJCAR 2018 - 9th International Joint Conference on Automated Reasoning. Core Ranking 2018: A*. Article. Extended Version.

“A Formally Verified Interpreter for a Shell-like Programming Language”. Nicolas Jeannerod, Claude Marché and Ralf Treinen. In VSTTE 2017 - 9th Working Conference on Verified Software: Theories, Tools and Experiments. Article.

“Le coquillage dans le CoLiS-mateur”. Nicolas Jeannerod. In JFLA 2017 - 28e Journées Francophones des Langages Applicatifs. Article. Archive.

See all my publications.

“Verification of Shell Scripts Performing File Hierarchy Transformations”. At PhD Thesis Defence.
Links: ⋅ Slides ⋅ Replay [MQ;LQ] ⋅ Dedicated Page ⋅ Thesis.

“Analysing installation scenarios of Debian Packages”. At IRIF's Verification Seminar.
Links: ⋅ Slides ⋅ Demo ⋅ Replay ⋅ Associated article.

“Symbolic Execution of Debian Packages”. At AVM'19.
Links: ⋅ Slides ⋅ Demo.

“Symbolic Execution of Maintainer Scripts”. With Ralf Treinen. At DebConf'19.
Links: ⋅ Slides ⋅ Demo ⋅ Replay [LQ] .

“Mining Debian Maintainer Scripts”. With Ralf Treinen. At DebConf'18.
Links: ⋅ Slides ⋅ Replay [LQ] .

“Deciding the First-Order Theory of an Algebra of Feature Trees with Updates”. At IJCAR'18.
Links: ⋅ Slides ⋅ Associated article.

“Deciding the First-Order Theory of an Algebra of Feature Trees with Updates”. At IRIF's Verification Seminar.
Links: ⋅ Slides ⋅ Associated article.

“Formalising an Intermediate Language for POSIX Shell”. With Yann Régis-Gianas. At Seminar Gallium.
Links: ⋅ Slides.

“A Formally Verified Interpreter for a Shell-like Programming Language”. At VSTTE'17.
Links: ⋅ Slides ⋅ Associated article.

“A Formally Verified Interpreter for a Shell-like Programming Language”. At Seminar VALS.
Links: ⋅ Slides.

“Le coquillage dans le CoLiS-mateur”. At JFLA'17.
Links: ⋅ Slides ⋅ Associated article.

See all my talks.

“Internet et outils”. Practical exercises at Université de Paris (France): Introduction to web programming in HTML5/CSS/PHP/MySQL/JS for first year students in computing.

“Principe de fonctionnement des machines binaires”. Written exercises at Université de Paris (France): Introduction to binary, circuits and processors for first year students in computing.

“Concepts informatiques”. Written exercises at Université de Paris (France): Introduction to compilation for first year students in computing.

“Programmation fonctionnelle”. Practical exercises at Université de Paris (France): Introduction to functional programming in OCaml for third year students in computing.

“Internet et outils”. Practical exercises at Université de Paris (France): Introduction to web programming in HTML5/CSS/PHP/MySQL/JS for first year students in computing.

“Concepts informatiques”. Written exercises at Université de Paris (France): Introduction to compilation for first year students in computing.

“Projet informatique”. Tutoring at Université de Paris (France): tutoring of second year students in computing during their programming project.

“Introduction à la programmation”. Practical exercises at Université de Paris (France): Introduction to programming in Java for first year students in computing.