> For the complete documentation index, see [llms.txt](https://docs.metatrust.io/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.metatrust.io/getting-started/how-to-use-security-prover.md).

# How to use Security Prover

Here is a step-by-step guide for using the scanning engine Security Prover on MetaScan based on the demo contract code. You can also watch the [video instructions](https://youtu.be/CatvrkcJTNk).  (Video Link: <https://youtu.be/CatvrkcJTNk>)

1. Upload the smart contract to MetaScan.\
   Click "Add Projects" and select "Upload Files" to add the project that needs scanning.

   <div><figure><img src="/files/B29hG2lWqGLy3XA62345" alt=""><figcaption></figcaption></figure> <figure><img src="/files/YdhtKJw3OahRSvhcCCIC" alt=""><figcaption></figcaption></figure></div>
2. Select the appropriate project type based on the situation. Here we select "Framework-less Solidity Files" and click "Continue".

   <figure><img src="/files/JEkc7dvcpiweBGrY3AXV" alt=""><figcaption></figcaption></figure>
3. Upload a zip file of the project and click "Continue".

   <figure><img src="/files/KfNgEjxND10YzoVj6IDo" alt=""><figcaption></figcaption></figure>
4. Input a project name and click "Upload" to upload the project.

   <figure><img src="/files/6RcbnoY4Dfh6wLzvcriL" alt=""><figcaption></figcaption></figure>
5. Configure contract analysis settings and scan. Click "Start Scan" to prepare for scanning.

   <figure><img src="/files/nVZK3qHiyGGVJJq0TcsP" alt=""><figcaption></figcaption></figure>
6. Select "Security Prover" and fill in the name of the contract to verify in "Entry Contract", here we fill in "Token". Then click "Start Scan" to start security scanning.

   <figure><img src="/files/eh5EjS6PBySWeaEDQKNJ" alt=""><figcaption></figcaption></figure>

   <figure><img src="/files/7KgIKXcRgvxANX7pDuA6" alt=""><figcaption></figcaption></figure>
7. Review key metrics and information from the report.

   <figure><img src="/files/fHyQrWGpxUNreHtjHZIu" alt=""><figcaption></figcaption></figure>
8. Click on "EquailzationOfTransferBalances" under "Rules" and check the "Call Trace" information based on violation.\
   From the information, we know the violated condition is `assert(balanceBefore == balanceAfter);`\
   From the "Rule Call Resolutions" on the right, we know that when msg.sender is the same as $to, it will violate the check condition

   <figure><img src="/files/R73u5GzZAiYu458Iy2sR" alt=""><figcaption></figcaption></figure>
9. Click on the "transfer" in the "Call Trace" to check deeper call stack information.\
   In `uint256 senderAmount = _balances[sender];` senderAmount is 20000\
   In `uint256 recipientAmount = _balances[recipient];` recipientAmount is 20000

   <figure><img src="/files/RzuqilKbgb6PZ3pRHI62" alt=""><figcaption></figcaption></figure>
10. After calling `_balances[sender] = senderAmount.sub(amount);`, `_balances[sender]` becomes 19900

    <figure><img src="/files/c9AA5gWPLUHzX7ZVBs9E" alt=""><figcaption></figcaption></figure>
11. After calling `_balances[recipient] = recipientAmount.add(amount);`, `_balances[recipient]` becomes 20100

    <figure><img src="/files/7yC2cCKXGAFFRJgXJYm9" alt=""><figcaption></figcaption></figure>

**Thus the assertion `assert(balanceBefore == balanceAfter);` is finally violated.**<br>