Skip to content

Latest commit

 

History

History
34 lines (20 loc) · 921 Bytes

README.md

File metadata and controls

34 lines (20 loc) · 921 Bytes

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: NFTv1 verification result

Verify NFT contract version 2

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

Result: NFTv1 verification result

Reach out to me

Koolex Twitter

License

MIT