News

  • [2021-11-30] Gave a talk on Algorand’s smart contract security at Decipher 2021 here
  • [2021-10-24] Added support for TEAL 5 in tealer here
  • [2021-09-20] Published the security audit report of Tinyman here
  • [2020-10-15] Created a K syntax highlighter for the Kakoune text editor here
  • [2020-07-28] Published a post annoucing a new engagement with Algorand to build formal tools for Algorand’s smart contract ecosystem 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