After 20+ years in academic and industrial research, I went independent in 2024. I now take on R&D projects as a contractor and secure Web3 grants with partners...

The paper on ChonkyBFT is out! It contains the protocol description, mathematical proofs of correctness, formal specification and verification in Quint, and experiments...

We have published the report on model checking of accountability in the 3-slot finality protocol for Ethereum Foundation...

We have finished Phase 1 of the work on Solarkraft after the award by SCF...

DevCon 2024 in Bangkok was amazing! I gave a short talk and participated in a panel...

This was my first DSS! So much great material compressed in several days Also, I gave a talk on model checking of ZKsync governance...

Invited talk on Pragmatic bounded model checking for TLA+ with Apalache at the 16th International Conference on Verified Software: Theories, Tools, and Experiments...

A detailed blogpost that summarizes our work on formal specification of ZKsync Governance and model checking of its properties...

Giving a talk on my home turf...

Apalache has moved from Informal Systems to github.com/apalache and apalache-mc.org....