Public findings
6
Achievements
Skillset
Worked with
Biography
Biography
I'm an independent auditor for Spearbit. I was previously with Runtime Verification, Inc where I worked on audits and security tooling. I have lead a number of Ethereum and Solana audits as well as deep protocol audits in Rust and Go.
On Urbit, I formalized Nock in K and built the property testing library %quiz.
I co-authored KWasm, a fully formal and executable semantics for WebAssembly. Among other things, I have used KWasm for formal verification work of Ethereum-Wasm (defunct) smart contracts; and of Substrate in 2019-2020, where we extended the semantics to support Substrate-native calls and added tooling for summarizing large function calls into succint claims to prove.
I have a MSc in Computer Science and a penchant for abstract algebra and programming languages.
Top competitions
View allContest | Position | Date | Payout |
|---|---|---|---|
alchemix-v3 | 24 / 207 | May 2025 | $558 |
Private reviews
View allEngagement | Project title | Timeframe | Researchers |
|---|---|---|---|
Silo Finance | Silo Finance Dynamic Kink Model | Sep 2025 - Sep 2025 | |
Eco Foundation | Eco Permit3 PR 28 & PR 37 | Sep 2025 - Sep 2025 | |
Sablier | Sablier Token Distribution | Aug 2025 - Aug 2025 | |
Monad Labs | Monad | Jul 2025 - Aug 2025 | +1 |
Alchemix | v3-poc | Feb 2025 - Mar 2025 |
Security portfolio
Title | Description |
|---|---|
| Tezos Dexter v2 Audit | Dexter is a decentralized exchange on Tezos. We used the K framework to formally verify entrypoints to the contract. |
| EDEN Zero-Knowledge Protocol | EDEN is a SNARK-friendly virtual machine and instruction set, based on the low-level functional language Nock, which is built around binary trees. These binary trees lend themselves exceptionally well to ZK operations as they are easily encoded into polynomials, and operating on them as such is very efficient. Runtime Verification were consulted on the paper to provide perspectives on the design and analyze the security of the architecture. |
| Alchemix v2 Audit | Alchemix is a lending and stablecoin protocol on Ethereum. The audit is an excellent example of using hand verification, where we construct important invariants and write mathematical proofs on them to convince ourselves, the developers, and anyone reading the report that the invariants hold. |
| EUROe Stablecoin Audit | EUROe is a stablecoin designed to comply with laws and regulations in Europe, making it suitable for institutional adaption. |
| Optimism Formal Verification | Optimism Labs engaged Runtime Verification to formally verify parts of their core contracts, particularly the contracts of the rollup itself, and verify that deposit events are always properly emitted. |
| Ojo L1 audit | Ojo is a lending app chain on Cosmos. We reviewed its node, price feeder, and core contracts deployed on top of the app chain. |