← Back to home

Writing

Collection of blogposts written for Informal Systems and my own thoughts on security engineering, blockchain protocols, and software development.

Case Study: Formalizing Grug's Jellyfish Merkle Tree with Quint↗FeaturedInformal Systems

·8 min read·
Security,Rust,Data Structures,Merkle Trees

Case study written with my colleagues Gabriela Moreira and Josef Widder for Informal Systems. A technical exploration of formally specifying the Jellyfish Merkle Tree data structure using Quint. We break down the space-efficient sparse Merkle tree implementation originally designed for Left Curve's Grug, translating its complex operations into formal specifications for better understanding and verification.

Case Study: Using Model-Based Testing with Quint to Secure Neutron's Liquidity Pool Migration↗FeaturedInformal Systems

·12 min read·
Security,Rust,Formal Methods,Model-based Testing,Quint

Case study written with my colleague Ivan Gavran for Informal Systems. How we used formal specification and model-based testing to verify the correctness of a critical liquidity pool migration for Neutron, the first consumer chain on Cosmos Hub. A deep dive into applying Quint for protocol verification in production systems.