这是一份针对Scallop借贷协议的全面形式化验证报告，详细阐述了验证的范围、方法和关键发现。报告通过形式化证明确保了协议在资金安全、管理功能、风险参数、余额表操作、借贷和清算机制以及算术运算方面的正确性。
