run Command Documentation

Description:

The kaas-cli run command executes Kontrol proofs either locally, within a Docker container, or remotely on KaaS infrastructure. Kontrol is an open-source formal verification tool for Ethereum smart contracts, maintained by Runtime Verification (Kontrol GitHub repository).

Requirements:

To run your tests you will need:

• For remote runs you must have a valid internet connection and license with the KaaS online platform at more info on the website. OR

• Kontrol must be installed locally. See Kontrol documentation for installation instructions. OR

• Docker must be installed locally. See Docker documentation for installation instructions.

• You must have at minimum a foundry.toml file at the root of you TEST directory.

• A kontrol.toml file is optional, but if present, it will be used to run the tests using specific configuraiton options passed to kontrol.

  • kontrol.toml is a kontrol specific configuration file that can be used to specify additional options for the proof run, and manage what kontrol does or does not do.

Usage:

kaas-cli run [OPTIONS]

Kaas CLI will attempt to run the tests within the current working directory. So long as a foundry.toml file is present, it will be used to run the tests. If no foundry.toml file is present, it will exit. If a kontrol.toml file is present, it will be used to run the tests using specific configuraiton options passed to kontrol.

If your execution directory for tests are within a subdirectory, either cd to that directory or use the --test-root flag to specify the path to the tests.

Key Environment Variables:

• FOUNDRY_PROFILE: Set the preferred profile for your kontrol tests. Example: export FOUNDRY_PROFILE=kprove

  Otherwise, the default profile will be used. And if no 'out' definition is provided here kaas-cli will fallback to using 'out' for dumping all kcfg proof files.

Key Options:

• --mode, -m: Specifies the execution mode. Accepted values are local, remote, or container.

  • local: Runs Kontrol proofs directly on the host machine. Requires Kontrol to be installed locally, see Kontrol documentation for installation instructions.

  • container: Executes proofs inside a Docker container on the host machine, ensuring a consistent and isolated environment.

  • remote: Submits proofs to KaaS remote compute infrastructure, requiring authentication and a valid vault specification.

• --watch, -w: Monitors the job execution status. If set, waits until the job is completed, applicable in all modes.

• --build-only, -bo: Only runs kontrol build without executing kontrol prove.

• --prove-only-profile, -pop: Runs kontrol prove on a previously built proof, without executing kontrol build. Requires a profile name.

• --kontrol-version, -kv: Specifies the Kontrol version. Defaults to "v0.0.0" if not provided (Kontrol releases on GitHub).

• --kontrol-docker-image, -kdi: Specifies the Docker image for running Kontrol in container mode.

• --url, -u: The API server URL. Defaults to the configured server URL and is typically used for development or testing environments.

• --vault-spec, -vs: Required in remote mode. Specifies the vault in <ORG_NAME>/<VAULT_NAME> format.

• --token, -t: A personal access key for authentication against the remote server. If not provided, you must authenticate using environment variables or device flow authentication.

• --branch, -b: (Optional) Specifies a Git branch for remote runs, aiding in reproducible CI/CD workflows.

• --test-root, -tr: Specifies the test folder root path relative to the project root.

• --extra-build-args, -eb: Additional arguments passed directly to kontrol build. For available options, consult the Kontrol Build Options documentation.

Execution Flow:

1. Local Mode: Calls kontrol build and kontrol prove directly on the host. Kontrol must be installed beforehand. If Kontrol is not found, the CLI will provide installation guidance (Kontrol Documentation).

2. Container Mode: Runs on the host machine. Uses a Docker container to run kontrol build and kontrol prove. This ensures an isolated environment with Kontrol installed without modifying the host system.

3. Remote Mode: Uses KaasClient to run proofs on the remote KaaS infrastructure. Requires --vault-spec and --token. If --watch is set, the CLI monitors the job until completion.

Error Handling and Output:

• --verbose, -v enables additional output useful for troubleshooting.

---

Example (Local Mode):

kaas-cli run --mode local --extra-build-args "--verbose" --extra-prove-args "--xml-test-report"

Example (Remote Mode):

kaas-cli run --mode remote --vault-spec <YOUR_ORGANIZATION>/<YOUR_VAULT>:<OPTIONAL_TAG> --token <YOUR_PERSONAL_ACCESS_KEY> --watch