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 TA 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 tooling, to enhance the developer experience around Scala program verification.

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 will be working with Prof. Thomas Bourgeat on a research project next semester. The main goal will be formalizing and verifying a recent result in theoretical computer science in the Lean theorem prover, both as a way to survey the existing best practices in mathematics formalization, and as a way to verify the correctness of the proposed proof.
• Formalizing high order calculi in Lean: in the context of CS452 - Foundations of Sofware, I formalized STLC and extended it with simple PL structures (product types and let bindings, the code can be found here). That was a lot of fun, but the original goal was to formalize more complex structures. I plan on extending the idea of this project to one of two paths:
  • including dependent types and polymorphism, potentially formalizing the Calculus of Constructions concisely and plainly.
  • formalizing the Verse calculus, a core calculus for functional logic programming. its syntax and semantics are described in the preprint paper, While it is not an inherently complex system, at least in terms of its type system, the logic programming semantics of the calculus are quite intricate and might require a lot of work to formalize.