Rikard Hjort
Lead security researcher at Spearbit. Web3 security auditor, formal verifier and Urbit enthusiast
Security portfolio
Name | Description | |
|---|---|---|
Tezos Dexter v2 Audit | Dexter is a decentralized exchange on Tezos. We used the K framework to formally verify entrypoints to the contract. | Read more |
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. | Read more |
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. | Read more |
EUROe Stablecoin Audit | EUROe is a stablecoin designed to comply with laws and regulations in Europe, making it suitable for institutional adaption. | Read more |
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. | Read more |
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. | Read more |