# 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>


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.metatrust.io/getting-started/how-to-use-security-prover.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.