Formal Verification slow down with Pact?

Question

I was going to implement this piece of code in my smart contract:

(defun absBug:integer (num:integer)
 ;; This property fails
 @model [(property (>= result 0))]
 (if (= (- (* (- num 6) (+ num 11)) (* 42 num)) (* (* 64 7) 52270780833))
     (- 1)
     (abs num)
 )

I was wondering since I am implementing formal verification, will there be any latency or slow down once I deploy this contract onto any chain? Or is calculation done once and stored going forward?

(I know my code spits out the correct answer which I would have to adjust after the fact)

Answer 1

No, it does not affect the latency or any other performance on chain.

The purpose of formal verification is to prove that the contract is bug-free and deployable, hence it is ran before deployment and not on the chain.

FYI when you develop on pact-web, it runs formal verification by default. However, if you're locally developing the contract on your machine, you'll need to run (verify 'contract-name) to run the formal verification and this is when all the calculation takes place.