Protocol audits and research

Protocol specification and verification. For the most recent work, see:

• Specification and model checking of BFT consensus for Matter Labs.

• Specification and Model-checking of the ZKsync Governance Protocol for Matter Labs.

For a recent example of research on reasoning about safety of consensus, see Model checking safety of Ben-Or’s Byzantine consensus with Apalache.

Code audits. I have a proven track record of submitting valid high and medium findings at Code4rena, Sherlock, and Hackerone, individually, as well as in a team. In addition to that, I was conducting several Web3 protocol audits while working at Informal Systems. Need a proof? DM.

Given my expertise, I am flexible to help you with a range of activities along the stack/confidence axes:

Stack:

• Consensus, e.g., Tendermint/CometBFT or your custom consensus
• Interchain communication, e.g, bridges and IBC
• Smart contracts and dApps, e.g., Soroban, Solidity, Cosmwasm

Confidence:

• Manual code review
• Fuzzing, e.g., using Medusa
• Protocol specification and analysis, e.g., in TLA⁺ and Quint
• Model checking, e.g., using TLC and Apalache
• Math proofs

If you think that your project is too big for one person, or you are short on time, I am connected to a network of researchers, including my former peers.