About

• This repository is all about the certora.
• I compile notes, and tricks about certora here.

ALPHA_TO_BE_EXPLORED

• Do certora official certora contests to strengthn spec writing game with monetary greed
• shadow audit aave all versions using certora and read official certora specs
  • After each version testing compeletion, read certora official specs to get pro level spec vision
  • REMEMBER AAVA IS CERTORA'S GIRLFRIEND, SO THEY MUST HAVE USED THEIR FULL_POWERS 😄

Un_Explored

• ghosts and hooks ? ;
• using config files, although not important but just for kick
• Built-in certora detectors
  • Read-only-reentrancy-builtin-detecor
  • other built-in detectors like overflows/underflows and sanity checks
• GAMBIT: MUTANT GENERATOR
  • consider gambit a sort of automatic bug injection tool
  • why to use it? in order to verify specs
• EQUIVALENCE TESTING
  • You wanna test whether two different function implementations behave same?
  • use equivalence

Go to the Docs

• latest
• tutDoc

Do These Exercises And More Importantly read spec files to get more idea how to setup environments effeciently

• EthCC excersises in certora github
• AAVE certora reports
• below_not_so_important
  • Certora/examples
  • tutorial-code
  • Certora/tutorials