Need help understanding formal verification of asynchronous FIFO

Hi everyone,

I’m new to formal verification and trying to learn how to apply it to an asynchronous FIFO design (different write and read clocks).
I don’t have much experience with this topic, so I’m not sure how to start what properties to write, how to set up the environment, or how to check correctness formally.