Royco Dawn is a non-custodial risk-tranching protocol that splits any yield source into two tranches with distinct risk profiles and corresponding yields. Certora performed formal verification of the Solidity smart contract code. The full report below includes the methodology, threat analysis, findings, specifications, verification results, and Royco responses.