Skip to content

Add AI prover rules for Answer#3

Open
beiraoCertora wants to merge 8 commits into
Certora:mainfrom
beiraoCertora:certora-ai-prover-answer-9539edd4-f09
Open

Add AI prover rules for Answer#3
beiraoCertora wants to merge 8 commits into
Certora:mainfrom
beiraoCertora:certora-ai-prover-answer-9539edd4-f09

Conversation

@beiraoCertora

Copy link
Copy Markdown
Contributor

This PR adds AI prover artifacts generated for Answer.

Design: SmokeTest/design.md
Threat model: None

Generated files:

  • certora/README.md
  • certora/run-ai-prover.sh
  • .gitignore
  • certora/specs/autospec_Answer_Function.spec
  • certora/specs/summaries/Answer_base_summaries.spec
  • certora/specs/summaries/Answer_call_resolution.spec
  • certora/confs/autospec_Answer_Function.conf
  • certora/mocks/DummyERC20Impl.sol

How to run Certora Prover:

  1. Export your Certora Prover API key:
export CERTORAKEY=<your-certora-api-key>
  1. From the repository root, run the generated helper script:
bash certora/run-ai-prover.sh

The script checks your local toolchain, installs or updates Python CLI tools into a repo-local certora/.certora-tools virtual environment with a one-week PyPI cooldown, prepares the required Solidity compiler binaries, and then runs:

certoraRun certora/confs/autospec_Answer_Function.conf

Note: certoraRun uploads the repository to Certora's cloud for verification.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant