Security: Formal Verification using Act [Simple NFT Contract]

We have two versions of contract specification:

• v1 doesn't check if minting reaches 3000 which is supposed to be the NFT max supply. Therefore, Act indicates the behaviour of mint function violates this requirement.
• v2 does check that. Thus, it passes the check!

Verify NFT contract version 1

act prove --file sec-fv-sample/spec/nftv1.act

Result:

Verify NFT contract version 2

act prove --file sec-fv-sample/spec/nftv2.act

Result:

Reach out to me

Koolex Twitter

License

MIT