This document describes the formal verification effort of Blend V1 using Certora’s Sunbeam Prover, a tool developed to verify Soroban smart contracts. The tool operates at the Wasm bytecode level. This work was undertaken from November 26, 2024. We finished verifying the property on January 15, 2025.