An example specification for a constant product pool.
These examples can serve as an introduction to CVL ( Certora Verification Language ). It also contains examples that are based on real-life code and the spec that have caught critical bugs.
To run the examples, use the provided configuration
cd ConstantProductPoolExample
certoraRun ConstantProductPoolExample/certora/conf/run.conf
Alternatively the Certora IDE VSCode Extension: