A small programming language which compiles to WASM.

A list of watched / yet-to-be-watched movies.

Octagonal constraints solver developed and verified in Coq for the FORVES2 project.

Translated specification of the SHA3 hash family of functions into Lean.

A verified implementation of the SHA3 hash family of functions in Rust. Verification was done in Lean.