In October 2024, Runtime Verification engaged with Cork Protocol to perform formal verification on their DeFi protocol. At Runtime Verification, we specialize in building rigorous, mathematically grounded proofs to ensure that smart contracts behave as intended under all possible inputs and scenarios. Our tool, Kontrol, is designed to integrate seamlessly with Solidity-based projects, enabling developers to write property-based tests in Solidity and leverage symbolic execution to verify them. The following document summarizes the key aspects of our formal verification engagement with Cork Protocol, focusing on the tests, invariants, and findings from this collaboration.