for random projects that have nowhere else to go.

• I built lean-symb out of frustration at the fact that there was nothing of the sort out there. If you’re here, it might be of interest or use to you! do have a look.
• Over the course of my life, I wrote a bunch of personal utilities in a variety of languages and technologies for very specific use cases I had. I learned a lot, but I wouldn’t call that code particularly useful. It’s kept on my github for archival purposes.

The Warblre Rocq mechanization of ECMAScript regexes has become the basis for formal reasoning about regex behavior, providing a faithful representation of the official specification to base theorems and properties on. However, this mechanization is four years out of date with recent spec updates, meaning that these results cannot be faithful to currently deployed regex features like buffer boundaries, modifiers, and the v-flag. The goal of this thesis is to update Warblre and its downstream projects to ES2027, developing the procedures and necessary tooling to ensure these updates are faithful and efficient.

The Kotlin compiler uses dataflow analysis for program optimization, but also as a typechecking tool, to verify well-typedness and reject malformed programs. This behavior has no formal study, and risks introducing unsoundnesses in the typechecker. As a first step to verifying it, we introduce Chartreux, a Lean framework to specialize dataflow analyses and prove their correctness wrt program semantics, and we apply it to show the soundness of two analyses taken from the Kotlin compiler: nullability with consequents and callsInPlace contracts.

This work was concluded with Marcin Wojnarowski, under the watchful and precious supervision of Kameliya Golova, and it was published at VSTTE 2026!

As a semester research project under Prof. Thomas Bourgeat, I tackled the formalization of the results published as The 2-Dimensional Constraint Loop Problem is Decidable (2024) by Guilmant et al. The formalization was carried out in Lean, making heavy use of Mathlib for the foundational mathematical results.

The project was a lot of fun, despite the heavy reliance on mathematics that were far above my puching weight. In the end, all of the machinery was formalized, and good progress was carried out on the main result in the 1D case. The 2D case follows a similar argument, and is deferred :(.

The project’s achievements, limitations, and main conclusions can be found in the presentation for a quick overview, and in the report.