This repository contains examples of Solana applications that can be formally verfied with the Certora Prover.
See the Certora Solana Prover documentation for instruction about how to install the prerequisites.
Furthermore, you will need to install just.
Each example has a certora
subdirectory which contains files to perform the formal verification.
Inside of certora/conf
there are several .conf
files which are the config files for certoraSolanaProver
and
run the rules in the example.
For instance, to run the verification on the first_example
run the following:
cd cvlr_by_example/first_example/certora/conf/`
certoraSolanaProver Default.conf
This will build the code and run the verification.