News

  • [2020-10-15] Created a K syntax highlighter for the Kakoune text editor here
  • [2020-07-15] Published a post on verifying Gasper’s finality mechanism in Coq here
  • [2019-12-12] Published a series of articles comparing K and Coq as language verification frameworks here
  • [2019-10-22] Published a post on modeling the Beacon Chain as an executable formal model in K here
  • [2019-10-11] We have two papers presented today at FMBC’19… Read more
  • [2019-06-18] Published a post on modeling and verifying Algorand’s security using Coq here

Research Interests

Formal methods for program verification, specification and design of distributed and concurrent programming languages and systems, and for analysis of security properties.

Most Recent Projects