Certora Formal Verification Rules

.github/workflows/certora-restaking.yaml

@@ -0,0 +1,39 @@
+name: Certora Prover (Restaking)
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+  workflow_dispatch:
+
+jobs:
+ certora_run_restaking_program:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+      - name: Apply Certora Patch
+        run: git apply certora/certora-mocks.patch
+      - name: Submit verification jobs to Certora Prover
+        uses: Certora/certora-run-action@v1
+        with:
+          configurations: |-
+            integrity.conf 
+            toggle-assert-false-rules.conf 
+            toggle.conf 
+            loader-assert-false-rules.conf 
+            loader.conf 
+          job-name: "restaking_program rules"
+          ecosystem: solana
+          working-directory: restaking_program/src/certora/confs
+          certora-key: ${{ secrets.CERTORAKEY }}
+          certora-sbf-options: "-vvv --tools-version=v1.43"
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/certora-vault.yaml

@@ -0,0 +1,38 @@
+name: Certora Prover (Vault)
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+  workflow_dispatch:
+
+jobs:
+  certora_run_vault_program:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+      - name: Apply Certora Patch
+        run: git apply certora/certora-mocks.patch
+      - name: Submit verification jobs to Certora Prover
+        uses: Certora/certora-run-action@v1
+        with:
+          configurations: |-
+            integrity.conf --commit_sha1 e8a773a5e7243238df1e2576cca7cfe56a99bb1b
+            access_control_checks.conf --commit_sha1 e8a773a5e7243238df1e2576cca7cfe56a99bb1b
+            toggle_checks.conf --commit_sha1 e8a773a5e7243238df1e2576cca7cfe56a99bb1b
+            fee.conf 
+          job-name: "vault_program rules"
+          ecosystem: solana
+          working-directory: vault_program/src/certora/confs
+          certora-key: ${{ secrets.CERTORAKEY }}
+          certora-sbf-options: "-vvv --tools-version=v1.43"
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

Cargo.toml

@@ -96,6 +96,11 @@ thiserror = "1.0.57"
 tokio = { version = "1.36.0", features = ["full"] }
 uriparse = "0.6.4"
 
+### CERTORA Dependencies
+cvlr = "0.4"
+cvlr-solana = { version = "0.5", git = "https://github.com/Certora/cvlr-solana.git", branch = "v0.5"} 
+
+
 [workspace.lints.rust.unexpected_cfgs]
 level = "warn"
 check-cfg = [