Receipt tree is a binary merkle tree of transaction receipts as described in SIMD. In this repository we provide a formal proof of security against merkle tree length extension attacks and malleability by formalizing the commitment scheme and adding preventive measures against the mentioned attacks.