how would one use certora to detect reentrancy vulnerability?
Reentrancy is something that is generally hard to check, and when you think about it it can actually accumulate into pretty computationally complex case with multiple calls from outside the contract to a method within the contract which itself can be exploited the same way. It creates a feedback loop and recursion cases that are generally hard to deal with.
With that said, there are ways you can approach reentrancy. Say you rely on calls to an external contract in your system - say an ERC20, a governance system or a custom data structure. You can create a malicious dummy implementation of this external contract and link/specify it in your script so that whenever this external contract or functions from it are called your malicious implementation kicks in.
For example, you can implement a malicious ERC20 that upon call to allowance/transfer call back one of your functions in the original contract, and so forth. Due to the computational complexity it is more likely that you will find a viable attack (if one exist), than succeed proving that a certain contract or even method is protected from reentrancy attacks. (edited)