Protocol audits

Protocol specification and verification. For the most recent work, see my blogpost on Specification and model checking of BFT consensus by Matter Labs.

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
• Interchain communication, e.g, bridges and IBC
• Smart contracts and dApps, e.g., Solidity, Cosmwasm, Cosmos SDK

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.