Search for a command to run...
Articles tagged with #cvl
Key Formal Verification Concepts for Smart Contracts 1. Logical Implications and Direction The direction of logical implications is crucial. Consider a rule restricting actions to owners: // Incorrect: Only checks if owners can change supply assert o...
Preconditions By adding preconditions, one can eliminate infeasible states and put constraints on values. The Rule totalSupplyAfterMintWithPrecondition is a copy of totalSupplyAfterMint with an additional constraint, shown in emphasis below: /** @tit...
Introduction Predicates, propositional logic and quantifiers are basic concepts of mathematical logic useful and needed when doing formal verification. Propositional Logic : basis of mathematical logic, dealing with boolean variables and operations....
