diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
new file mode 100644
index 0000000..36b7d7d
--- /dev/null
+++ b/.github/workflows/main.yml
@@ -0,0 +1,25 @@
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+  workflow_dispatch:
+
+jobs:
+  test:
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+    uses: ./.github/workflows/workflow.yml@main
+    secrets:
+      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      CERTORAKEY: ${{ secrets.CERTORAKEY }}
+    with:
+      use-beta: true
+      configurations: |-
+        tests/conf1.conf
+        tests/conf2.conf
+      solc-versions: 0.7.6 0.8.1
diff --git a/.github/workflows/workflow.yml b/.github/workflows/workflow.yml
new file mode 100644
index 0000000..256aea4
--- /dev/null
+++ b/.github/workflows/workflow.yml
@@ -0,0 +1,301 @@
+# yaml-language-server: $schema=https://raw.githubusercontent.com/SchemaStore/schemastore/refs/heads/master/src/schemas/json/github-workflow.json
+name: Reusable Workflow
+on:
+  workflow_call:
+    inputs:
+      cli-version:
+        required: false
+        type: string
+        description: |-
+          The version of the `certora-cli` to use. If not specified, the latest version
+          will be used.
+
+          Example:
+
+          ```yaml
+          cli-version: 7.0.0
+          ```
+      configurations:
+        required: true
+        type: string
+        description: |-
+          List of paths to configuration files to use for the `certoraRun` command.
+
+          Example:
+
+          ```yaml
+          configurations: |-
+            certConfigs/config1.conf
+            certConfigs/config2.conf
+            certConfigs/config3.conf
+          ```
+      solc-versions:
+        required: true
+        type: string
+        description: |-
+          List of Solidity versions to use for the `certoraRun` command.
+
+          Example:
+
+          ```yaml
+          solc-versions: |-
+            0.5.16
+            0.6.12
+            0.7.6
+          ```
+      solc-remove-version-prefix:
+        required: false
+        type: string
+        description: |-
+          The prefix to remove from the Solidity version when saving binaries.
+      server:
+        required: true
+        default: production
+        type: string
+        description: |-
+          The server to run the tests on. Default is `production`.
+          Options: `production`, `staging`, or `vaas-dev`.
+      use-alpha:
+        required: false
+        type: boolean
+        description: |-
+          Whether to use the alpha version of the `certora-cli`.
+      use-beta:
+        required: false
+        type: boolean
+        description: |-
+          Whether to use the beta version of the `certora-cli`.
+      add-status:
+        required: true
+        default: true
+        type: boolean
+        description: |-
+          Whether to add status checks to the commit.
+
+    secrets:
+      CERTORAKEY:
+        required: true
+
+env:
+  GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+jobs:
+  certora_run:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ref: feat/initial-setup
+      - name: Fetch Relevant Commit SHA for the Event
+        run: |
+          COMMIT_SHA=""
+          if [[ "${{ github.event_name }}" == "pull_request" ]]; then
+            COMMIT_SHA="${{ github.event.pull_request.head.sha }}"
+          elif [[ "${{ github.event_name }}" == "push" ]]; then
+            COMMIT_SHA="${{ github.sha }}"
+          elif [[ "${{ github.event_name }}" == "workflow_run" ]]; then
+            COMMIT_SHA="${{ github.event.workflow_run.head_commit.id }}"
+          elif [[ "${{ github.event_name }}" == "commit_comment" ]]; then
+            COMMIT_SHA="${{ github.event.comment.commit_id }}"
+          elif [[ "${{ github.event_name }}" == "issue_comment" ]]; then
+            COMMIT_SHA="${{ github.event.comment.commit_id }}"
+          elif [[ "${{ github.event_name }}" == "pull_request_review" ]]; then
+            COMMIT_SHA="${{ github.event.review.commit_id }}"
+          elif [[ "${{ github.event_name }}" == "pull_request_review_comment" ]]; then
+            COMMIT_SHA="${{ github.event.comment.commit_id }}"
+          else
+            COMMIT_SHA="$(git rev-parse HEAD)"
+          fi
+          echo "COMMIT_SHA=${COMMIT_SHA}" >> $GITHUB_ENV
+          echo "SHORT_COMMIT_SHA=${COMMIT_SHA:0:12}" >> $GITHUB_ENV
+
+      - name: Group ID and Message
+        run: |
+          echo "MESSAGE_SUFFIX=GH:${{ github.repository }}/${SHORT_COMMIT_SHA}" >> $GITHUB_ENV
+          echo "GROUP_ID=$(cat /proc/sys/kernel/random/uuid)" >> $GITHUB_ENV
+
+      - name: Cache CLI Dependencies Key
+        run: echo "${{ inputs.cli-version }}-${{ inputs.use-alpha }}-${{ inputs.use-beta }}" > .certora-cache
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@v4
+        with:
+          enable-cache: true
+          cache-dependency-glob: .certora-cache
+
+      - name: Install certora-cli
+        run: |
+          CERT_CLI_PACKAGE="certora-cli"
+            if [ '${{ inputs.use_alpha }}' == 'true' ]; then
+              CERT_CLI_PACKAGE="certora-cli-alpha"
+            elif [ '${{ inputs.use_beta }}' == 'true' ]; then
+              CERT_CLI_PACKAGE="certora-cli-beta"
+            fi
+          CERT_CLI_PACKAGE="${CERT_CLI_PACKAGE}${CERT_CLI_VERSION:+==$CERT_CLI_VERSION}"
+          echo "CERT_CLI_PACKAGE=$CERT_CLI_PACKAGE" >> $GITHUB_ENV
+          uv tool install "$CERT_CLI_PACKAGE"
+        env:
+          CERT_CLI_VERSION: ${{ inputs.cli_version }}
+
+      - name: Cache Solidity Binaries
+        id: solc-cache
+        uses: actions/cache@v4
+        with:
+          path: /opt/solc-bin
+          key: solc-bin
+
+      - name: Add Solidity to Github Path
+        run: echo "/opt/solc-bin/" >> $GITHUB_PATH
+
+      - name: Download Solidity Binaries
+        run: |
+          mkdir -p /opt/solc-bin
+          VERSIONS="${{ inputs.solc-versions }}"
+          GH_LINK='https://api.github.com/repos/ethereum/solidity/releases/tags/v'
+          JQ_FILTER='.assets[] | select(.name == "solc-static-linux") | .url'
+          AUTH_HEADER="Authorization: Bearer ${GITHUB_TOKEN}"
+
+          for version in $VERSIONS; do
+            version="${version#v}"
+            if [ -z "${{ inputs.solc-remove-version-prefix }}" ]; then
+              use_version=$version
+            else
+              use_version="${version#${{ inputs.solc-remove-version-prefix }}}"
+            fi
+
+            BIN_PATH="/opt/solc-bin/solc$use_version"
+
+            if [ ! -f "$BIN_PATH" ]; then
+              echo "Downloading Solidity $version"
+              RELEASE_DETAIL=$(curl -sH "$AUTH_HEADER" "${GH_LINK}${version}")
+
+              if [[ -z "$RELEASE_DETAIL" || $(jq 'has("assets")' <<< "$RELEASE_DETAIL") == "false" ]]; then
+                echo "Failed to fetch release details for Solidity $version"
+                echo "$RELEASE_DETAIL"
+                exit 1
+              fi
+              BIN_LINK=$(jq -r "$JQ_FILTER" <<< "$RELEASE_DETAIL")
+
+              curl -L \
+                -H "Accept: application/octet-stream" \
+                -H "$AUTH_HEADER" \
+                "${BIN_LINK}" -o "$BIN_PATH"
+
+              # Verify the binary
+              chmod +x "$BIN_PATH"
+              "solc$use_version" --version
+            fi
+          done
+
+          ls -1 /opt/solc-bin/
+
+      - name: Sanitize confugurations
+        run: |
+          CONFIGURATIONS="${{ inputs.configurations }}"
+          for conf in $CONFIGURATIONS; do
+            echo "Sanitizing $conf"
+            tmp_conf=$(mktemp)
+            jq 'del(.wait_for_results)' $conf > $tmp_conf
+            mv $tmp_conf $conf
+          done
+
+      - name: Run Certora
+        id: certora-run
+        run: |
+          CONFIGURATIONS="${{ inputs.configurations }}"
+          MAX_MSG_LEN=254
+          SUFFIX_LEN=${#MESSAGE_SUFFIX}
+          REMAINING_LEN=$((MAX_MSG_LEN - SUFFIX_LEN))
+          jobs=0
+
+          LOG_DIR="/tmp/certora-logs/"
+          mkdir -p "$LOG_DIR"
+
+          for conf in $CONFIGURATIONS; do
+            echo "Starting $conf"
+
+            if [[ ${#conf} -gt $conf_max_length ]]; then
+              msg_conf=${conf: -$REMAINING_LEN}
+            else
+              msg_conf=$conf
+            fi
+
+            # Create log files
+            STDOUT="$LOG_DIR/$conf.stdout"
+            mkdir -p "$(dirname "$STDOUT")"
+            STDERR="$LOG_DIR/$conf.stderr"
+            mkdir -p "$(dirname "$STDERR")"
+
+            uvx --from "$CERT_CLI_PACKAGE" certoraRun \
+              $conf \
+              --msg "${msg_conf} ${MESSAGE_SUFFIX}" \
+              --server "${{ inputs.server }}" \
+              --group_id "${GROUP_ID}" \
+              --send_only \
+              --wait_for_results none >"$STDERR" 2>"$STDERR" &
+
+            ((jobs++)) || true
+          done
+
+          # Wait for all jobs to finish and mark if any failed
+          total_ret=0
+          failed_jobs=0
+          for conf in $CONFIGURATIONS; do
+            ret=0
+            wait -n || ret=$?
+            if [ $ret -ne 0 ]; then
+              ((jobs--)) || true
+              ((failed_jobs++)) || true
+              total_ret=$ret
+            fi
+          done
+
+          # Add jobs to output
+          echo "total_jobs=$jobs" >> $GITHUB_OUTPUT
+          echo "failed_jobs=$failed_jobs" >> $GITHUB_OUTPUT
+
+          # Remove empty log files
+          find "$LOG_DIR" -type f -empty -delete
+
+          if [ $ret -ne 0 ]; then
+            echo "Some configurations failed! Please check the logs."
+            exit $ret
+          fi
+
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+      - name: Add GH Status
+        if: ${{ inputs.add-status }}
+        run: |
+          curl -L \
+            -X POST \
+            -H "Accept: application/vnd.github+json" \
+            -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+            -H "X-GitHub-Api-Version: 2022-11-28" \
+            https://api.github.com/repos/${{ github.repository }}/statuses/$COMMIT_SHA \
+            -d '{"state":"pending","target_url":"https://prover.certora.com","description":"0/${{ steps.certora-run.outputs.total_jobs }} jobs finished.","context":"certora-run"}'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Upload Logs
+        uses: actions/upload-artifact@v4
+        id: upload-logs
+        if: always()
+        with:
+          name: logs
+          path: /tmp/certora-logs/*
+
+      # Add comment with log link
+      - name: Add Comment With Logs Link
+        if: ${{ steps.upload-logs.outputs.artifact-url }}
+        run: |
+          curl -L \
+            -X POST \
+            -H "Accept: application/vnd.github+json" \
+            -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+            -H "X-GitHub-Api-Version: 2022-11-28" \
+            https://api.github.com/repos/${{ github.repository }}/commits/$COMMIT_SHA/comments \
+            -d '{"body":"# Started Certora Run\n\n- Started ${{ steps.certora-run.outputs.total_jobs }} jobs\n- ${{ steps.certora-run.outputs.failed_jobs }} jobs failed\n\n[Logs](${{ steps.upload-logs.outputs.artifact-url }})\n"}'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..9741e8a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,411 @@
+/tmp
+emv-*
+.certora_internal/
+
+# MacOS
+# General
+.DS_Store
+.AppleDouble
+.LSOverride
+
+# Icon must end with two \r
+Icon
+
+# Thumbnails
+._*
+
+# Files that might appear in the root of a volume
+.DocumentRevisions-V100
+.fseventsd
+.Spotlight-V100
+.TemporaryItems
+.Trashes
+.VolumeIcon.icns
+.com.apple.timemachine.donotpresent
+
+# Directories potentially created on remote AFP share
+.AppleDB
+.AppleDesktop
+Network Trash Folder
+Temporary Items
+.apdisk
+
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+#  Usually these files are written by a python script from a template
+#  before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+!tests/*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage*
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+cover/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+.pybuilder/
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+#   For a library or package, you might want to ignore these files since the code is
+#   intended to run in multiple environments; otherwise, check them in:
+# .python-version
+
+# pipenv
+#   According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+#   However, in case of collaboration, if having platform-specific dependencies or dependencies
+#   having no cross-platform support, pipenv may install dependencies that don't work, or not
+#   install all needed dependencies.
+#Pipfile.lock
+
+# poetry
+#   Similar to Pipfile.lock, it is generally recommended to include poetry.lock in version control.
+#   This is especially recommended for binary packages to ensure reproducibility, and is more
+#   commonly ignored for libraries.
+#   https://python-poetry.org/docs/basic-usage/#commit-your-poetrylock-file-to-version-control
+#poetry.lock
+
+# pdm
+#   Similar to Pipfile.lock, it is generally recommended to include pdm.lock in version control.
+#pdm.lock
+#   pdm stores project-wide configurations in .pdm.toml, but it is recommended to not include it
+#   in version control.
+#   https://pdm.fming.dev/#use-with-ide
+.pdm.toml
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow and github.com/pdm-project/pdm
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/
+
+# pytype static type analyzer
+.pytype/
+
+# Cython debug symbols
+cython_debug/
+
+# VS Code
+.vscode/*
+# !.vscode/settings.json
+# !.vscode/tasks.json
+# !.vscode/launch.json
+# !.vscode/extensions.json
+# !.vscode/*.code-snippets
+
+# Local History for Visual Studio Code
+.history/
+
+# Built Visual Studio Code Extensions
+*.vsix
+
+# Covers JetBrains IDEs: IntelliJ, RubyMine, PhpStorm, AppCode, PyCharm, CLion, Android Studio, WebStorm and Rider
+# Reference: https://intellij-support.jetbrains.com/hc/en-us/articles/206544839
+
+# User-specific stuff
+.idea/**/workspace.xml
+.idea/**/tasks.xml
+.idea/**/usage.statistics.xml
+.idea/**/dictionaries
+.idea/**/shelf
+
+# AWS User-specific
+.idea/**/aws.xml
+
+# Generated files
+.idea/**/contentModel.xml
+
+# Sensitive or high-churn files
+.idea/**/dataSources/
+.idea/**/dataSources.ids
+.idea/**/dataSources.local.xml
+.idea/**/sqlDataSources.xml
+.idea/**/dynamic.xml
+.idea/**/uiDesigner.xml
+.idea/**/dbnavigator.xml
+
+# Gradle
+.idea/**/gradle.xml
+.idea/**/libraries
+
+# Gradle and Maven with auto-import
+# When using Gradle or Maven with auto-import, you should exclude module files,
+# since they will be recreated, and may cause churn.  Uncomment if using
+# auto-import.
+# .idea/artifacts
+# .idea/compiler.xml
+# .idea/jarRepositories.xml
+# .idea/modules.xml
+# .idea/*.iml
+# .idea/modules
+# *.iml
+# *.ipr
+
+# CMake
+cmake-build-*/
+
+# Mongo Explorer plugin
+.idea/**/mongoSettings.xml
+
+# File-based project format
+*.iws
+
+# IntelliJ
+out/
+
+# mpeltonen/sbt-idea plugin
+.idea_modules/
+
+# JIRA plugin
+atlassian-ide-plugin.xml
+
+# Cursive Clojure plugin
+.idea/replstate.xml
+
+# SonarLint plugin
+.idea/sonarlint/
+
+# Crashlytics plugin (for Android Studio and IntelliJ)
+com_crashlytics_export_strings.xml
+crashlytics.properties
+crashlytics-build.properties
+fabric.properties
+
+# Editor-based Rest Client
+.idea/httpRequests
+
+# Android studio 3.1+ serialized cache file
+.idea/caches/build_file_checksums.ser
+Footer
+
+# Logs
+logs
+*.log
+npm-debug.log*
+yarn-debug.log*
+yarn-error.log*
+lerna-debug.log*
+.pnpm-debug.log*
+
+# Diagnostic reports (https://nodejs.org/api/report.html)
+report.[0-9]*.[0-9]*.[0-9]*.[0-9]*.json
+
+# Runtime data
+pids
+*.pid
+*.seed
+*.pid.lock
+
+# Directory for instrumented libs generated by jscoverage/JSCover
+lib-cov
+
+# Coverage directory used by tools like istanbul
+coverage
+*.lcov
+
+# nyc test coverage
+.nyc_output
+
+# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files)
+.grunt
+
+# Bower dependency directory (https://bower.io/)
+bower_components
+
+# node-waf configuration
+.lock-wscript
+
+# Compiled binary addons (https://nodejs.org/api/addons.html)
+build/Release
+
+# Dependency directories
+node_modules/
+jspm_packages/
+
+# Snowpack dependency directory (https://snowpack.dev/)
+web_modules/
+
+# TypeScript cache
+*.tsbuildinfo
+
+# Optional npm cache directory
+.npm
+
+# Optional eslint cache
+.eslintcache
+
+# Optional stylelint cache
+.stylelintcache
+
+# Microbundle cache
+.rpt2_cache/
+.rts2_cache_cjs/
+.rts2_cache_es/
+.rts2_cache_umd/
+
+# Optional REPL history
+.node_repl_history
+
+# Output of 'npm pack'
+*.tgz
+
+# Yarn Integrity file
+.yarn-integrity
+
+# dotenv environment variable files
+.env
+.env.development.local
+.env.test.local
+.env.production.local
+.env.local
+
+# parcel-bundler cache (https://parceljs.org/)
+.cache
+.parcel-cache
+
+# Next.js build output
+.next
+out
+
+# Nuxt.js build / generate output
+.nuxt
+dist
+
+# Gatsby files
+.cache/
+# Comment in the public line in if your project uses Gatsby and not Next.js
+# https://nextjs.org/blog/next-9-1#public-directory-support
+# public
+
+# vuepress build output
+.vuepress/dist
+
+# vuepress v2.x temp and cache directory
+.temp
+.cache
+
+# Docusaurus cache and generated files
+.docusaurus
+
+# Serverless directories
+.serverless/
+
+# FuseBox cache
+.fusebox/
+
+# DynamoDB Local files
+.dynamodb/
+
+# TernJS port file
+.tern-port
+
+# Stores VSCode versions used for testing VSCode extensions
+.vscode-test
+
+# yarn v2
+.yarn/cache
+.yarn/unplugged
+.yarn/build-state.yml
+.yarn/install-state.gz
+.pnp.*
+**.idea**
diff --git a/tests/Invertible.sol b/tests/Invertible.sol
new file mode 100644
index 0000000..bffdf92
--- /dev/null
+++ b/tests/Invertible.sol
@@ -0,0 +1,16 @@
+contract InvertibleBroken {
+	address public admin;
+	uint public counter;
+		
+	function inc() public returns (uint) {
+		require(msg.sender == admin);
+		return ++counter;
+	}
+	
+	function dec() public returns (uint) {
+		require(msg.sender == admin);
+		return --counter;
+	}
+}
+
+
diff --git a/tests/Invertible.spec b/tests/Invertible.spec
new file mode 100644
index 0000000..df6432b
--- /dev/null
+++ b/tests/Invertible.spec
@@ -0,0 +1,23 @@
+methods {
+	function counter() external returns uint256 envfree;
+}
+
+rule invertible {
+	/* `foo(args)` - process function `foo` with arguments `args` 
+		and assume that it does not revert */
+	uint256 curr = counter();
+	/* The `env` type represents the EVM parameters passed in every
+	   call (msg., tx., block.* variables in Solidity)
+	 */
+	env e;  
+	/* For non-`envfree` methods, the environment is passed as the first argument*/
+	inc(e);
+	dec(e);
+	assert counter() == curr, "dec followed by inc should give the original value";
+}
+
+rule monotone {
+	uint256 curr = counter();
+	env e;  
+	assert inc(e) > curr, "Incremented value is greater than original value";
+}
diff --git a/tests/conf1.conf b/tests/conf1.conf
new file mode 100644
index 0000000..376fe8d
--- /dev/null
+++ b/tests/conf1.conf
@@ -0,0 +1,9 @@
+{
+    "files": [
+        "tests/Invertible.sol:InvertibleBroken"
+    ],
+    "process": "emv",
+    "solc": "solc0.7.6",
+    "verify": "InvertibleBroken:tests/Invertible.spec",
+    "wait_for_results": "all"
+}
diff --git a/tests/conf2.conf b/tests/conf2.conf
new file mode 100644
index 0000000..619aec2
--- /dev/null
+++ b/tests/conf2.conf
@@ -0,0 +1,8 @@
+{
+    "files": [
+        "tests/Invertible.sol:InvertibleBroken"
+    ],
+    "process": "emv",
+    "solc": "solc8.1",
+    "verify": "InvertibleBroken:tests/Invertible.spec"
+}
diff --git a/workflow.yml b/workflow.yml
new file mode 100644
index 0000000..256aea4
--- /dev/null
+++ b/workflow.yml
@@ -0,0 +1,301 @@
+# yaml-language-server: $schema=https://raw.githubusercontent.com/SchemaStore/schemastore/refs/heads/master/src/schemas/json/github-workflow.json
+name: Reusable Workflow
+on:
+  workflow_call:
+    inputs:
+      cli-version:
+        required: false
+        type: string
+        description: |-
+          The version of the `certora-cli` to use. If not specified, the latest version
+          will be used.
+
+          Example:
+
+          ```yaml
+          cli-version: 7.0.0
+          ```
+      configurations:
+        required: true
+        type: string
+        description: |-
+          List of paths to configuration files to use for the `certoraRun` command.
+
+          Example:
+
+          ```yaml
+          configurations: |-
+            certConfigs/config1.conf
+            certConfigs/config2.conf
+            certConfigs/config3.conf
+          ```
+      solc-versions:
+        required: true
+        type: string
+        description: |-
+          List of Solidity versions to use for the `certoraRun` command.
+
+          Example:
+
+          ```yaml
+          solc-versions: |-
+            0.5.16
+            0.6.12
+            0.7.6
+          ```
+      solc-remove-version-prefix:
+        required: false
+        type: string
+        description: |-
+          The prefix to remove from the Solidity version when saving binaries.
+      server:
+        required: true
+        default: production
+        type: string
+        description: |-
+          The server to run the tests on. Default is `production`.
+          Options: `production`, `staging`, or `vaas-dev`.
+      use-alpha:
+        required: false
+        type: boolean
+        description: |-
+          Whether to use the alpha version of the `certora-cli`.
+      use-beta:
+        required: false
+        type: boolean
+        description: |-
+          Whether to use the beta version of the `certora-cli`.
+      add-status:
+        required: true
+        default: true
+        type: boolean
+        description: |-
+          Whether to add status checks to the commit.
+
+    secrets:
+      CERTORAKEY:
+        required: true
+
+env:
+  GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+jobs:
+  certora_run:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ref: feat/initial-setup
+      - name: Fetch Relevant Commit SHA for the Event
+        run: |
+          COMMIT_SHA=""
+          if [[ "${{ github.event_name }}" == "pull_request" ]]; then
+            COMMIT_SHA="${{ github.event.pull_request.head.sha }}"
+          elif [[ "${{ github.event_name }}" == "push" ]]; then
+            COMMIT_SHA="${{ github.sha }}"
+          elif [[ "${{ github.event_name }}" == "workflow_run" ]]; then
+            COMMIT_SHA="${{ github.event.workflow_run.head_commit.id }}"
+          elif [[ "${{ github.event_name }}" == "commit_comment" ]]; then
+            COMMIT_SHA="${{ github.event.comment.commit_id }}"
+          elif [[ "${{ github.event_name }}" == "issue_comment" ]]; then
+            COMMIT_SHA="${{ github.event.comment.commit_id }}"
+          elif [[ "${{ github.event_name }}" == "pull_request_review" ]]; then
+            COMMIT_SHA="${{ github.event.review.commit_id }}"
+          elif [[ "${{ github.event_name }}" == "pull_request_review_comment" ]]; then
+            COMMIT_SHA="${{ github.event.comment.commit_id }}"
+          else
+            COMMIT_SHA="$(git rev-parse HEAD)"
+          fi
+          echo "COMMIT_SHA=${COMMIT_SHA}" >> $GITHUB_ENV
+          echo "SHORT_COMMIT_SHA=${COMMIT_SHA:0:12}" >> $GITHUB_ENV
+
+      - name: Group ID and Message
+        run: |
+          echo "MESSAGE_SUFFIX=GH:${{ github.repository }}/${SHORT_COMMIT_SHA}" >> $GITHUB_ENV
+          echo "GROUP_ID=$(cat /proc/sys/kernel/random/uuid)" >> $GITHUB_ENV
+
+      - name: Cache CLI Dependencies Key
+        run: echo "${{ inputs.cli-version }}-${{ inputs.use-alpha }}-${{ inputs.use-beta }}" > .certora-cache
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@v4
+        with:
+          enable-cache: true
+          cache-dependency-glob: .certora-cache
+
+      - name: Install certora-cli
+        run: |
+          CERT_CLI_PACKAGE="certora-cli"
+            if [ '${{ inputs.use_alpha }}' == 'true' ]; then
+              CERT_CLI_PACKAGE="certora-cli-alpha"
+            elif [ '${{ inputs.use_beta }}' == 'true' ]; then
+              CERT_CLI_PACKAGE="certora-cli-beta"
+            fi
+          CERT_CLI_PACKAGE="${CERT_CLI_PACKAGE}${CERT_CLI_VERSION:+==$CERT_CLI_VERSION}"
+          echo "CERT_CLI_PACKAGE=$CERT_CLI_PACKAGE" >> $GITHUB_ENV
+          uv tool install "$CERT_CLI_PACKAGE"
+        env:
+          CERT_CLI_VERSION: ${{ inputs.cli_version }}
+
+      - name: Cache Solidity Binaries
+        id: solc-cache
+        uses: actions/cache@v4
+        with:
+          path: /opt/solc-bin
+          key: solc-bin
+
+      - name: Add Solidity to Github Path
+        run: echo "/opt/solc-bin/" >> $GITHUB_PATH
+
+      - name: Download Solidity Binaries
+        run: |
+          mkdir -p /opt/solc-bin
+          VERSIONS="${{ inputs.solc-versions }}"
+          GH_LINK='https://api.github.com/repos/ethereum/solidity/releases/tags/v'
+          JQ_FILTER='.assets[] | select(.name == "solc-static-linux") | .url'
+          AUTH_HEADER="Authorization: Bearer ${GITHUB_TOKEN}"
+
+          for version in $VERSIONS; do
+            version="${version#v}"
+            if [ -z "${{ inputs.solc-remove-version-prefix }}" ]; then
+              use_version=$version
+            else
+              use_version="${version#${{ inputs.solc-remove-version-prefix }}}"
+            fi
+
+            BIN_PATH="/opt/solc-bin/solc$use_version"
+
+            if [ ! -f "$BIN_PATH" ]; then
+              echo "Downloading Solidity $version"
+              RELEASE_DETAIL=$(curl -sH "$AUTH_HEADER" "${GH_LINK}${version}")
+
+              if [[ -z "$RELEASE_DETAIL" || $(jq 'has("assets")' <<< "$RELEASE_DETAIL") == "false" ]]; then
+                echo "Failed to fetch release details for Solidity $version"
+                echo "$RELEASE_DETAIL"
+                exit 1
+              fi
+              BIN_LINK=$(jq -r "$JQ_FILTER" <<< "$RELEASE_DETAIL")
+
+              curl -L \
+                -H "Accept: application/octet-stream" \
+                -H "$AUTH_HEADER" \
+                "${BIN_LINK}" -o "$BIN_PATH"
+
+              # Verify the binary
+              chmod +x "$BIN_PATH"
+              "solc$use_version" --version
+            fi
+          done
+
+          ls -1 /opt/solc-bin/
+
+      - name: Sanitize confugurations
+        run: |
+          CONFIGURATIONS="${{ inputs.configurations }}"
+          for conf in $CONFIGURATIONS; do
+            echo "Sanitizing $conf"
+            tmp_conf=$(mktemp)
+            jq 'del(.wait_for_results)' $conf > $tmp_conf
+            mv $tmp_conf $conf
+          done
+
+      - name: Run Certora
+        id: certora-run
+        run: |
+          CONFIGURATIONS="${{ inputs.configurations }}"
+          MAX_MSG_LEN=254
+          SUFFIX_LEN=${#MESSAGE_SUFFIX}
+          REMAINING_LEN=$((MAX_MSG_LEN - SUFFIX_LEN))
+          jobs=0
+
+          LOG_DIR="/tmp/certora-logs/"
+          mkdir -p "$LOG_DIR"
+
+          for conf in $CONFIGURATIONS; do
+            echo "Starting $conf"
+
+            if [[ ${#conf} -gt $conf_max_length ]]; then
+              msg_conf=${conf: -$REMAINING_LEN}
+            else
+              msg_conf=$conf
+            fi
+
+            # Create log files
+            STDOUT="$LOG_DIR/$conf.stdout"
+            mkdir -p "$(dirname "$STDOUT")"
+            STDERR="$LOG_DIR/$conf.stderr"
+            mkdir -p "$(dirname "$STDERR")"
+
+            uvx --from "$CERT_CLI_PACKAGE" certoraRun \
+              $conf \
+              --msg "${msg_conf} ${MESSAGE_SUFFIX}" \
+              --server "${{ inputs.server }}" \
+              --group_id "${GROUP_ID}" \
+              --send_only \
+              --wait_for_results none >"$STDERR" 2>"$STDERR" &
+
+            ((jobs++)) || true
+          done
+
+          # Wait for all jobs to finish and mark if any failed
+          total_ret=0
+          failed_jobs=0
+          for conf in $CONFIGURATIONS; do
+            ret=0
+            wait -n || ret=$?
+            if [ $ret -ne 0 ]; then
+              ((jobs--)) || true
+              ((failed_jobs++)) || true
+              total_ret=$ret
+            fi
+          done
+
+          # Add jobs to output
+          echo "total_jobs=$jobs" >> $GITHUB_OUTPUT
+          echo "failed_jobs=$failed_jobs" >> $GITHUB_OUTPUT
+
+          # Remove empty log files
+          find "$LOG_DIR" -type f -empty -delete
+
+          if [ $ret -ne 0 ]; then
+            echo "Some configurations failed! Please check the logs."
+            exit $ret
+          fi
+
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+      - name: Add GH Status
+        if: ${{ inputs.add-status }}
+        run: |
+          curl -L \
+            -X POST \
+            -H "Accept: application/vnd.github+json" \
+            -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+            -H "X-GitHub-Api-Version: 2022-11-28" \
+            https://api.github.com/repos/${{ github.repository }}/statuses/$COMMIT_SHA \
+            -d '{"state":"pending","target_url":"https://prover.certora.com","description":"0/${{ steps.certora-run.outputs.total_jobs }} jobs finished.","context":"certora-run"}'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Upload Logs
+        uses: actions/upload-artifact@v4
+        id: upload-logs
+        if: always()
+        with:
+          name: logs
+          path: /tmp/certora-logs/*
+
+      # Add comment with log link
+      - name: Add Comment With Logs Link
+        if: ${{ steps.upload-logs.outputs.artifact-url }}
+        run: |
+          curl -L \
+            -X POST \
+            -H "Accept: application/vnd.github+json" \
+            -H "Authorization: Bearer ${GITHUB_TOKEN}" \
+            -H "X-GitHub-Api-Version: 2022-11-28" \
+            https://api.github.com/repos/${{ github.repository }}/commits/$COMMIT_SHA/comments \
+            -d '{"body":"# Started Certora Run\n\n- Started ${{ steps.certora-run.outputs.total_jobs }} jobs\n- ${{ steps.certora-run.outputs.failed_jobs }} jobs failed\n\n[Logs](${{ steps.upload-logs.outputs.artifact-url }})\n"}'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}