Verify contracts in: $ARGUMENTS
Verifies SLOP contract consistency using Z3 theorem prover and suggests fixes.
/plugin marketplace add rhinoman/slop-plugin/plugin install rhinoman-slop@rhinoman/slop-pluginVerify contracts in: $ARGUMENTS
Run slop verify on the specified SLOP file(s) to check contract consistency using Z3.
Run the verifier:
slop verify <file.slop>
Analyze the output:
For each failure or warning, provide:
@pre, @post, or range type)Postcondition not satisfied by implementation:
;; Problem: @post claims result > 0, but implementation can return 0
(@post {$result > 0})
(if (> x 0) x 0) ; Returns 0 when x <= 0
;; Fix: Adjust postcondition or implementation
(@post {$result >= 0}) ; Weaker postcondition
;; OR
(if (> x 0) x 1) ; Ensure result > 0
Precondition too weak:
;; Problem: Division by zero possible
(@pre {y >= 0}) ; Allows y = 0
(/ x y)
;; Fix: Strengthen precondition
(@pre {y > 0})
Range type violation:
;; Problem: Result can exceed range bounds
(type Percentage (Int 0 .. 100))
(fn calc ((in x Int))
(@spec ((Int) -> Percentage))
(* x 2)) ; Can exceed 100
;; Fix: Clamp or validate
(if (> (* x 2) 100) 100 (* x 2))
Warnings indicate issues the verifier detected but can't fully verify yet:
When suggesting fixes:
@pre over weakening @post (fail fast)@intent matches the contract - maybe the contract is wrongFor each file:
/verifySmart verification command - run quality checks and final verification