K as a Service (KaaS) VS Code Extension

KaaS provides integration with powerful compute backend with the intelligent and capable kontrol frontend. We've simplified and now kaas is available directly in your IDE!

Features

• Detects and works with kontrol.toml files and foundry.toml
• These files are not required but recommended for organizing your test env and runtime requirements
• Kaas-VsCode provides remote comptue for heavy verification jobs running kontrol.

Getting Started

1. Install the extension from the Marketplace.
2. Open a folder containing your test code.
3. Use the left-hand command palette to access KaaS Compute resources
4. Get the results back on your machine.

Configuration

Get API key from https://kaas.runtimeverification.com

Design Specification & New Features

Dirty Git Detection

• Before submitting a job to KaaS, the extension checks for uncommitted or unpushed changes in the git repository.
• If dirty, the user is prompted to either "Proceed Anyway" or "Cancel". Canceling aborts the job submission.

GitHub App Access Check

• If KaaS cannot access the remote repository (e.g., no git info), the user is notified and given a button to install the Runtime Verification GitHub App.
• The extension links directly to: https://github.com/apps/runtime-verification-inc

kcfg File Download

• Users can download kcfg files generated by a job using the command palette or context menu.
• The extension fetches a presigned download URL from the KaaS API and saves the file locally.

KaaS API Integration

• The extension uses the KaaS API for job submission, status polling, and artifact (kcfg) download.
• Endpoints used include:
  • /api/orgs/{organizationName}/vaults/{vaultName}/jobs (job submission)
  • /api/jobs/{jobId}/files/{fileName}/url (artifact download)

User Flows

• Job Submission:
  1. User triggers a job.
  2. Extension checks git status. If dirty, prompts user.
  3. Extension checks for remote access. If missing, prompts user to install GitHub App.
  4. If all checks pass, job is submitted to KaaS.
• kcfg Download:
  1. User invokes the download command for a job/test.
  2. User enters the kcfg file name and selects a save location.
  3. Extension downloads the file from KaaS and saves it locally.