Certora Formal Verification

[kel-certora]

Add Certora formal verification specs and CI

This PR introduces Certora's formal verification of the Suilend liquid staking protocol, along with a GitHub Actions workflow to run verification automatically on PRs against main.

What's included

Formal Specification

Verification rules under certora/spec/ covering 10 property groups:

• Solvency and exchange rate monotonicity
• Total SUI supply accounting
• Token supply initialization invariants
• Value conservation (mint/redeem)
• Fee accounting integrity
• Supply control authorization
• No-arbitrage guarantee
• Validator registry consistency and integrity
• Assumption validation

For details on individual rules, assumptions, and running instructions, see certora/README.md file.

CI Integration

Contains a workflow file .github/workflows/certora.yml thats runs the full Certora verification suite on PRs targeting the main (and the certora branch), using the Certora/certora-run-action. Verification jobs are run in the Certora cloud and results are posted back to the PR via GITHUB_TOKEN. Requires a CERTORAKEY repository secret to be set to a valid Certora key.

Note on munges

Verification requires patching the source code before running, mainly to widen the visibility of internal functions. These patches live in certora/munges/ and must be kept in sync with the source. If the patched files change, verification will fail to apply and CI will break. See the README for instructions on maintaining regenerating patches.