# Security Prover Prover is a dynamic scanning engine that runs code and explores the state space of all its execution processes. During exploration, Prover detects vulnerabilities based on execution characteristics such as property changes and execution paths. Meanwhile, Prover can prove the absence of critical vulnerabilities like reentrancy through sufficient constraint conditions. Thus, the Prover engine both detects vulnerabilities and verifies the existence of critical vulnerabilities in the code. To implement the Prover product, we built a symbolic execution engine based on the semantic layer, supporting automatic generation of code state spaces and allowing users to write Prover scripts in Solidity to mine state spaces. Prover's vulnerability detection includes: compiling contract files to generate AST trees, dynamically executing statements and recording the process. Finally, it determines whether there are vulnerabilities based on the state space, execution paths, and built-in rules. Prover's safety proofs define safety proof conditions for each type of vulnerability, such as reentrancy, after obtaining the state space, thereby proving that corresponding vulnerabilities will not occur in the code. Prover's property proofs use user-defined MAIN functions to verify that contract properties do not violate rules during contract execution. Compared to static engines, Prover has higher reliability and lower false alarm rates because the code state spaces it analyzes are truly executable. --- # 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/introduction/metascan/security-prover.md?ask= ``` 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.