Diaframe-inspired automation tactic for Iris Lean

Lean port of the Iris higher-order separation logic

A verified implementation of the SHA3 hash family of functions in Rust, using the Aeneas framework

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

Math bachelor's thesis at UCM on category theory

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

A small programming language which compiles to WASM.