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.

As a semester research project under Prof. Thomas Bourgeat, I formalized a large chunk of the paper The 2D constraint loop is decidable, published in 2024 by researchers at MPI-SWS. The project was carried out in the Lean theorem proving environment, with heavy use of the Mathlib library.

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

Stainless is a verification framework for the Scala programming language developed by the LARA lab at EPFL. It provides a rich set of features on top of Scala to integrate code and its specification, and a verification engine that relies on a combination of automated techniques to prove that the program satisfies the given spec. In the context of student assistant work for CS550 - Formal Verification, I am currently working on extending the tooling around the framework with a VSCode extension, to provide an easier way to interact with the framework.

Inspired by the tooling for other similar tools, like Dafny and Lean 4, the aim is to better integrate the framework into developer tools.

The project is still in its very early stages, but it will be open-sourced soon.

In the context of CS428 - Interactive Theorem Proving, we implemented Steele, a verified decompilation framework for WebAssembly. It relies on the lifting of WebAssembly modules to a higher-level theoretical representation, FLInt, on which decompilation passes introduce new abstractions and deobfuscations. Every pass is implemented in Rocq and verified, ensuring the correctness of the whole decompilation process.

For the course project, we implemented and verified the lifting pass, as well as a proof of concept pass introducing pointer dereferencing. Additionally, we attempted the extraction of an OCaml executable from our Rocq proofs, but that is still very much a work in progress. We plan to continue working on this project on and off, exploring new directions and integrations.

The project’s code can be found on codeberg, along with the PDF report.

Beyond more work on the projects here mentioned, there are multiple projects in the pipeline, including:

I’m currently reading on the formalization and implementation of higher-order calculi in Lean: the long term goal is implementing a dependently-typed programming language, with a simple tactic mode, while documenting the journey in a “theorem proving from scratch” series of reports.

I’m also interested in formalizing the Verse calculus, a core calculus for functional logic programming. Its syntax and semantics are described in the preprint paper, which looks really interesting, and probably a lot of fun to formalize.