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
- [2021] Formal tooling for Algorand’s smart contract architecture
- [2020] Verification of finality in Gasper
- [2019] An executable model of the Beacon Chain protocol
- [2019] Verification of Algorand’s safety property
- [2019] Statistical model checking of RANDAO against attacks
- [2018] Resource-bounded intruders in denial of service attacks
- [2018] Modeling and verification of distance fraud attacks