Jasmin allows developing high-performance, assembly level cryptographic primitives that are both ISA-agnostic and can be formally verified for: functional correctness, security against side-channel attacks and security against crypto-analysis. For this project we implemented and verified the post-quantum signature scheme 'CROSS' in Jasmin.

An optimizing, functional SSA-based compiler written in Rust hosting a frontend, intermediate transformations and a backend. The compiler utilizes the GVN_PRE transformation to optimize programs in SSA form, and an SMT solver for register allocation.

Bachelor's thesis and conference paper about adding dynamic optimization (aka Just-In-Time compilation) to WebAssembly on constrained devices (e.g. microcontrollers, system-on-chips).

Lossless file compression algorithms implemented in Rust.