The Informal Blog - Case Study: Formalizing Grug’s Jellyfish Merkle Tree with Quint