Mehdi Bouaziz

I am a Principal Software Engineer at SkipLabs, building a platform for reactive backend services.
I am also co-founder of Atacama, providing technical advisory in blockchain, smart contracts, static analysis, programming languages, and competitive programming.

Previously, I was a Staff Software Engineer and TechLead at Nomadic Labs (2019-2024), leading protocol development for Tezos blockchain. Before that, I was a Senior Research Scientist at Facebook (Meta) (2015-2019) working on the Zoncolan and the Infer static analyzer for large-scale code analysis.

I was a bronze medalist (2004, Athens, Greece) and a gold medalist (2005, Nowy Sącz, Poland) at the International Olympiads in Informatics (IOI), a bronze medalist (2005, Sárospatak, Hungary) at the Central-European Olympiad in Informatics (CEOI), as well as a world finalist (2010, Harbin, China) at the International Collegiate Programming Contest (ACM-ICPC).

Projects

Skip (2024 – Present)
Skip is an open-source framework for building reactive backend services. It is based on a custom-built native backend for efficient reactive computation, allowing your system to deliver up-to-date and correct results without requiring any bug-prone manual dependency tracking and updating. TypeScript interfaces and abstractions are provided so that you can write a reactive service using standard tools while also taking advantage of the Skip framework's abstractions for efficient reactivity.

Tezos blockchain protocol (2019 – 2024)
Led development of protocol features for Tezos upgrades including Adaptive Issuance, new staking mechanisms, Michelson smart contract language improvements, consensus algorithms (Emmy*, Tenderbake), Liquidity Baking, Sapling privacy features, and Tickets capability-based tokens.

Infer static analyzer (2016 – 2019)
Infer is a static analysis tool - if you give Infer some Java or C/C++/Objective-C code it produces a list of potential bugs. Anyone can use Infer to intercept critical bugs before they have shipped to users, and help prevent crashes or poor performance.

Zoncolan (2015 – 2017)
Static taint analysis for security at Facebook scale. Designed and implemented information-flow abstract domains for Hack/PHP allowing security engineers to identify precise potentially harmful flows of information in hundreds of millions of lines of code.

Pyre type checker (2016 – 2017)
Early reviewer of Facebook's static type checker for Python, providing feedback on design and implementation during development phase.

AnaStaSec (2015 – 2018)
AnaStaSec is a four years ANR project, that is supported by the ANR (French national research agency). The main objective of this project is to show that formal methods are mature enough to be used for proving the security of large-scale software intensive industrial systems during the development and the production of these systems. The security properties of software-intensive industrial case studies will be formally specified and then proved automatically, thanks to a set of prototype tools that will be designed during the project. We focus on the analysis of some case studies provided by Airbus. More precisely, the secrecy and the authenticity of messages in cryptographic protocols envisioned to secure datalink communications will be addressed at model and implementation levels.

Clousot / CodeContracts (2011 – 2012)
Static checker for .NET based on abstract interpretation. Developed cloud-based version (Cloudot), object invariants inference algorithms, effective caching systems, and version-based metrics analysis tools.

SAGE (2011)
Whitebox fuzzing for security testing. Redesigned SAGE for larger scale with distributed fuzzing, fault-tolerance, job migration, job sharding, and UI improvements for scalability and security testing of Microsoft Office.

Jsx (2010 – 2011)
Symbolic interpreter for JavaScript developed as part of a static security analyzer at Stevens Institute of Technology. Designed for security analysis of web applications through symbolic execution.

Research

Research interests: programming languages, semantics, abstract interpretation, static analysis, computer security, blockchain protocols, reactive systems.

Collaborations

GOSPEL (2022 – 2024)
Vers un langage de spécification et un écosystème pour spécifier, tester et vérifier des programmes OCaml. A specification language and ecosystem for specifying, testing and verifying OCaml programs. Collaboration with François Pottier and partners.

SALTO (2021 – 2024)
Static Analyses for Trustworthy OCaml. Collaboration with Inria and Nomadic Labs. Partners: Benoît Montagu, Pierre Lermusiaux, Thomas Jensen, Thomas Genet.

CAVOC (2022 – 2024)
Compositional Automated Verification of OCaml. Collaboration with Inria and Nomadic Labs. Partners: Hamza Jaâfar, Guilhem Jaber, Gabriel Radanne, Laure Gonnord.

Ciao-PP for Michelson (2019 – 2024)
Analysis and Verification of the Resource Consumption of Tezos Contracts using Ciao-PP. Collaboration with IMDEA Software Institute and Tezos Foundation. Led by Manuel Hermenegildo.

Inferbo (2016 – 2017)
Collaboration with Seoul National University and Professor Kwangkeun Yi on buffer overrun analysis for the Infer static analyzer.

Publications

Guillaume Bau, Antoine Miné, Vincent Botbol, and Mehdi Bouaziz, Abstract Interpretation of Michelson smart-contracts, in Static Analysis and Operations of Programming Languages (SOAP@PLDI 2022), ACM, June 2022. 📄

Ezgi Çiçek, Mehdi Bouaziz, Sungkeun Cho, and Dino Distefano, Static Resource Analysis at Scale, in Static Analysis Symposium (SAS 2020), Springer, November 2020. 📄

Michael Barnett, Mehdi Bouaziz, Manuel Fähndrich, and Francesco Logozzo, A case for static analyzers in the cloud, in 8th Workshop on Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode 2013), Elsevier, March 2013. 📄

Mehdi Bouaziz, Francesco Logozzo, and Manuel Fähndrich, Inference of Necessary Field Conditions with Abstract Interpretation, in 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), Springer, December 2012. 📄

Mehdi Bouaziz, TreeKs: A Functor to Make Numerical Abstract Domains Scalable, in 4th International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2012), Elsevier, September 2012. 📄

Mehdi Bouaziz, Jsx: a symbolic evaluator for JavaScript, Stevens Institute of Technology, February 2011. 📄

Mehdi Bouaziz, TreeKs: un foncteur pour faire passer les domaines numériques à l'échelle, Master's thesis, École normale supérieure, August 2010. 📄

Mathieu Barbin and Mehdi Bouaziz, A Unified Library of Primitives for QML/Opa Compilers and Interpreters, MLstate, September 2009. 📄

Mehdi Bouaziz, Optimized Client-Server Distribution of Ajax Web Applications, MLstate, September 2009. 📄

Mehdi Bouaziz, Approximation statique de propriétés d'applications web, MLstate, September 2008. 📄

🔗 All publications (BibTeX)

Talks

SWERC 2023-2024 Problem Analysis. Southwestern European Programming Contest, January 2024. 📺

Dev Success: What is Adaptive Issuance?. YouTube presentation, September 2023. 📺

Adaptive Inflation Overview. Internal presentation, April 2023. 📄

Analysis & Verification of the Resource Consumption of Tezos Contracts (Ciao-PP). NL Research Seminar (host), April 2022. 📺

Helmholtz - A Verifier for Tezos Smart Contracts. NL Research Seminar (host), April 2021. 📺

SWERC 2020-21 Problem Analysis. Southwestern European Programming Contest, March 2021. 📺

Tezos Town Hall: Exploring Edo. Podcast, January 2021. 🎧 🔗

SWERC 2019-2020 Problem Analysis. Southwestern European Programming Contest, January 2020. 📺

Building Your Own Modular Static Analyser with Infer. POPL 2019 TutorialFest, Lisbon, Portugal, January 2019. 🔗

SWERC 2018 Problem Analysis. Southwestern European Programming Contest, 2018. 📺

SWERC 2017 Problem Analysis. Southwestern European Programming Contest, 2017.

Invited Talk. Principles and Practice of Declarative Programming (PPDP) 2016, Edinburgh, Scotland, September 2016.

CodeContracts & Clousot. Course on Abstract Interpretation, East China Normal University, Shanghai, China, November 26, 2013.

Scalable Numerical Abstract Domains. 2nd Workshop on Analysis and Verification of Dependable Cyber Physical Software (AVDCPS 2013), National University of Defense Technology, Changsha, China, November 23, 2013. 📊

Spécification et vérification de programmes avec CodeContracts. 2e Forum méthodes formelles (FMF 2013), Laboratoire d'Analyse et d'Architecture des Systèmes, Toulouse, France, June 28, 2013. 📊

A case for static analyzers in the cloud. 8th Workshop on Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode 2013), Rome, Italy, March 2013. 📊

Inference of Necessary Field Conditions with Abstract Interpretation. 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), Kyoto, Japan, December 2012. 📊

TreeKs: A Functor to Make Numerical Abstract Domains Scalable. 4th International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2012), Deauville, France, September 2012. 📊

Inference of object invariants. Microsoft Research Faculty Summit 2012, Redmond, WA, USA, July 2012. 📊

Object invariants inference with CodeContracts. Microsoft Research, Redmond, WA, USA, July 2011. 📊

Distributed whitebox fuzzing for security testing. Microsoft Research, Redmond, WA, USA, July 2011. 📊

Symbolic execution for JavaScript. Stevens Institute of Technology, Hoboken, NJ, USA, February 2011. 📊

TreeKs: un foncteur pour faire passer les domaines numériques à l'échelle. Master's defense, École normale supérieure, Paris, France, August 2010. 📊

Optimized Client-Server Distribution of Ajax Web Applications. MLstate, Edinburgh, UK, August 2009.

Teaching

Teaching Assistant at Université Paris Cité (September 2013 – August 2016)
Taught Bachelor students: Introduction to CS & programming (Java), Computer science concepts, Advanced programming in C, Introduction to algorithms (Python), Programming projects.

Vocational Trainer at Ville de Paris (September 2014 – October 2014)
Training librarians of Paris how to teach programming as part of educational outreach and computer science literacy programs.

Invited Coach for the Egyptian Training camp for the International Olympiad in Informatics (June 2015)
Invited teacher for a summer camp to train and teach algorithmics to high school Egyptian students for the International Olympiad in Informatics.

Competitive Programming Mentor at France-IOI (2006 – Present)
Course development, mentoring during training camps, task creation for the International Olympiad in Informatics. Translation, proofreading, and educational content development for algorithmic training.

Member of the organization of Castor Informatique (January 2012 – January 2016)
My activities involve preparing tasks, translating, proofreading, and improving them; testing the platform; participating in the international Bebras Task Workshop in 2015 (Sankt Pölten, Austria) where I presented the France country report.

Students

PhD Student: Guillaume Bau (2020 – 2024)

Interns:

Academic Community Activities

Program Committee Member:

Reviewer and Grant Activities:

International Olympiad in Informatics:

Competition Judge:

Rock Climbing

Volunteer at International Rock Climbing Competitions (September 2021 – October 2023)
Balayer for Lead and Speed, brusher for Bouldering, usher, cameraman, handler, logistics at:

Rock climbing monitor (September 2021 – June 2022)
Co-supervising rock climbing courses for children.

Rock climbing instructor at FFCAM | Fédération française des Clubs Alpins et de Montagne (March 2015 – September 2017)
Certified rock climbing instructor for the French Alpine Club Federation.

Contact

LinkedIn | CV | GitHub | GitLab | Google Scholar | gpg public key

Place

These days, you can probably find me in Lille, France.

Last update: April 2, 2025