About Me

/ 1 MIN READ

Hi, I’m Matteo Busi.

I am a researcher specializing in formal methods applied to security. My work lives at the intersection of security and mathematical certainty and I build tools and frameworks that ensure software does exactly what it is supposed to do, and nothing else.

Tools & Open Source

I am a firm believer in open-source security tools. Some of my contributions include:

  • StrandsRocq: A framework for cryptographic protocol verification that emphasizes proof reuse and automation.
  • ALVIE: An OCaml-based hardware verification tool that reduced analysis time for trusted execution environments from months to hours.

Technical Stack

  • Theorem Proving: Rocq (Coq), Lean4.
  • Programming: OCaml, Rust, Python, C.

Find me on GitHub / Google Scholar

< prev |

home