## Problem:

Smart contract code can have bugs. To reduce any possibility of bugs they are formally verified. Problem with formal specification is that the specification itself needs to know what the code intends to do. For ex: Bank contract won't want balance to be in negative. But the formal specification might not know that it may check for integer overflow but not whether it always remains positive. That part is identified by humans and then they update the formal specification.

The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of theCertora Prover are scoped to the provided specification, and any cases not covered by the specification are not checked by the Certora Prover.


## Solution:

The properties are generated by humans based on domain knowledge. That's why they create a database of rules to identify similar contracts

and rules. This similar rules give LLM some domain knowledge as to what is expected from the contract.

They also provide llm with similar example from their vast vector database. Prover was 38K LOC. They made a custom compiler for PSL and they integrated it with solidity compiler. They are using a prover to check if the smart contract follows the generated property specification.

For matching they are identifying a single function (system under test) in a contract and match similar rules/functions in their vector database.

Domain Knowledge:

1. Properties are: what. What this function should satisfy?
2. Rule is how, so in specification language.
3. Invariant is what must be always true for your contract to be safe.