About

I’m a compiler and formal verification engineer. I work on machine-checked correctness for real systems, in Rocq (formerly Coq), Lean 4 and Isabelle. I also host the Type Theory Forall podcast.

Recently I built a compiler from a stack bytecode to x86-64, verified in Rocq against Jasmin’s model of the instruction set. AI agents wrote the proofs; the work that was mine was designing a specification they could not weaken. I’m also formalizing Tarski’s undefinability theorem in Lean 4, and I mentor students applying to graduate programmes in programming languages and theorem proving.

Before that I did formal specification of a verifiable voting protocol at Free & Fair, and smart-contract semantics at Pruvendo. I completed my MSc at Purdue under Prof. Benjamin Delaware, translating OCaml GADTs into Rocq for rocq-of-ocaml, partly funded by Nomadic Labs. I’m a co-author of a POPL 2023 paper on divide-and-conquer recursion in Coq.

In summer 2019 I interned at Galois, verifying Amazon’s s2n TLS implementation with SAW. In 2018 I interned at SiFive with Murali Vijayaraghavan, formalizing a RISC-V floating-point unit in Coq and Kami.

I received my B.Sc. in Computer Science from the University of Brasília in 2017, advised by Prof. Rodrigo Bonifácio.

More in my CV and research.

Contact

Pedro da Costa Abreu Júnior
Email pedro ‘at’ typetheoryforall.com
GitHub github.com/pedrotst
LinkedIn linkedin.com/in/pedroabreu0
Twitter twitter.com/p_droabreu0