GitHub - nican0r/eBTC-certora-vs-echidna: Repository for blog post comparing differences between the Certora Prover and Trail of Bits' Echidna

This repo contains tests for comparing the Certora Prover with Trail of Bits' Echidna fuzzer.

Setup

The Certora tests are contained in the specs folder.

The tests were created to verify the following properties from the README:

AP-04 - the total collateral in active pool should be equal to the sum of all individual CDP collateral (run with certoraRun eBTC-certora-vs-echidna/certora/confs/AP04.conf)
BO-07 - eBTC tokens are burned upon repayment of a CDP's debt (run with certoraRun eBTC-certora-vs-echidna/certora/confs/BO07.conf)
CDPM-06 - redemptions do not increase a CDPs debt (run with certoraRun eBTC-certora-vs-echidna/certora/confs/CDPM06.conf)

Name		Name	Last commit message	Last commit date
Latest commit History 64 Commits
.github/workflows		.github/workflows
.vscode		.vscode
.yarn/releases		.yarn/releases
certora		certora
filter-repo		filter-repo
images		images
packages/contracts		packages/contracts
scripts		scripts
.gitattributes		.gitattributes
.gitignore		.gitignore
.gitmodules		.gitmodules
.prettierrc.json		.prettierrc.json
.solhint.json		.solhint.json
.yarnrc		.yarnrc
Dockerfile		Dockerfile
Invariants.MD		Invariants.MD
LICENSE		LICENSE
README.md		README.md
README_EBTC.md		README_EBTC.md
Whale Sniper.MD		Whale Sniper.MD
codecov.yml		codecov.yml
ngrok.config.template.yml		ngrok.config.template.yml
package.json		package.json
package.public.json		package.public.json
requirements.txt		requirements.txt
tsconfig.base.json		tsconfig.base.json
yarn.lock		yarn.lock
yarn.public.lock		yarn.public.lock