@ramilmust

Formal Verification, часть 2 .conf файл Конфигурационный файл и этим все сказано. Хранит в себе пути к исследуемым контрактам, к файлу спецификации, содержит настройки прувера Имеет расширение .conf, пишется как JSON Типичный файл выглядит так { "files": [ "./src/OurContract.sol:OurContract", "./src/AnotherContract.sol:AnotherContract" ], "verify": "OurContract:certora/spec/OurContractInvariant.spec", "wait_for_results": "all", "rule_sanity": "basic", "optimistic_loop": true, "msg":"Verification of OurContractInvariant" } После разделов files и verify находятся настройки анализа, альтернативно их можно писать в CLI при вызове команды certoraRun, которая запускает верификацию То есть можно было бы написать certoraRun ./certora/conf/OurContract.conf --verify OurContract:certora/spec/OurContractInvariant.spec --wait_for_results all --rule_sanity basic --optimistic_loop true --msg Verification of OurContractInvariant Кроме прочего таким образом могут быть заданы настройки самого прувера После запуска команды certoraRun компилируются контракты, затем проверяется корректность локально, если все ок, то задача уходит в работу на сервер, когда будет готово - вам пришлют ссылку на отчет Потому что Certora работает по freemium модели и вам доступны 2000 минут работы сервиса в месяц https://t.me/web3securityresearch

0 reply

0 recast

5 reactions