formal verification using certora prover