verilib-cli

A command-line tool for managing Verilib repositories, verification structure files, and API interactions.

Features

Secure Authentication - Store API keys safely using system keyring
Repository Management - Initialize, deploy, pull, and reclone repositories
Verification Structure - Create and manage verification goals with probe-verus integration
Cross-Platform - Works on macOS, Linux, and Windows

Execution Modes

verilib-cli supports two execution modes for verification commands (atomize, specify, verify):

Docker (Recommended): Runs probe-verus in a container with all dependencies pre-installed. This ensures a consistent environment and avoids local setup issues. You simply need Docker installed and running.
Local: Runs probe-verus directly on your host machine. This requires you to install probe-verus and all its dependencies (Rust, Verus, etc.) manually.

During initialization (verilib-cli init), you will be prompted to choose your preferred execution mode. You can also change it later by editing the .verilib/config.json file.

Note for Local Mode: If you choose to run locally and encounter issues with missing dependencies or environment configuration, please refer to the probe-verus repository for installation instructions and troubleshooting.

Installation

One-Line Installers (Recommended)

Linux & macOS:

curl -sSL https://github.com/Beneficial-AI-Foundation/verilib-cli/releases/latest/download/verilib-cli-installer.sh | sh

Windows (PowerShell):

irm https://github.com/Beneficial-AI-Foundation/verilib-cli/releases/latest/download/verilib-cli-installer.ps1 | iex

NPM (Cross-platform):

npm install -g verilib-cli

Package Managers

Homebrew (macOS):

brew tap Beneficial-AI-Foundation/verilib-cli
brew install verilib-cli

Windows MSI Installer: Download the latest .msi installer from the releases page.

Manual Installation

Download the appropriate binary from the releases page:

Platform	File
macOS (Apple Silicon)	`verilib-cli-aarch64-apple-darwin.tar.xz`
macOS (Intel)	`verilib-cli-x86_64-apple-darwin.tar.xz`
Linux (x86_64)	`verilib-cli-x86_64-unknown-linux-gnu.tar.xz`
Linux (ARM64)	`verilib-cli-aarch64-unknown-linux-gnu.tar.xz`
Windows	`verilib-cli-x86_64-pc-windows-msvc.zip`

Extract the archive and place the binary in your PATH.

Quick Start

Repository Workflow

# 1. Authenticate
verilib-cli auth

# 2. Initialize repository
verilib-cli init --id <repo-id>    # From existing ID
verilib-cli init                    # Create new (auto-detects git URL)

# 3. Work with repository
verilib-cli pull      # Pull latest changes
verilib-cli deploy    # Deploy changes
verilib-cli reclone   # Trigger server reclone

Verification Workflow

# 1. Create structure files
verilib-cli create

# 2. Enrich with atom metadata
verilib-cli atomize --update-stubs

# 3. Manage specifications
verilib-cli specify

# 4. Run verification
verilib-cli verify

Auto-Validation for Trusted Specs

For high-trust projects where all specifications are considered valid by default (e.g., in CI environments), you can enable auto-validation.

Add the following to your .verilib/config.json:

{
  "auto-validate-specs": true
}

When enabled, verilib-cli specify will automatically generate specification certificates for all uncertified specifications instead of prompting interactively. This is ideal for CI workflows.

Repository Commands

`auth`

Authenticate with the Verilib API. Your API key is stored securely in your system's keyring.

verilib-cli auth

`status`

Display current authentication status.

verilib-cli status

`init`

Initialize a repository from an existing ID or create a new one from a git URL.

verilib-cli init --id <repository-id>   # From existing ID
verilib-cli init                         # Create new repository

Options:

Option	Description
`--id <id>`	Initialize from existing repository ID
`--url <url>`	Custom API base URL

When creating a new repository (no --id), the CLI will:

Auto-detect git URL from current directory
Prompt for repository URL (supports branches and subfolders)
Collect metadata (language, proof language, summary)
Create repository and save ID locally

`deploy`

Deploy repository changes to the server.

verilib-cli deploy

Options:

Option	Description
`--url <url>`	Custom API base URL

`pull`

Pull the latest repository structure from the server.

verilib-cli pull

`reclone`

Trigger a reclone operation on the server. Includes safety checks for uncommitted changes.

verilib-cli reclone

Structure Commands

Commands for managing verification structure files. These integrate with probe-verus for static analysis.

Prerequisites

Install proof tools (Verus, Verus Analyzer, SCIP):

git clone https://github.com/Beneficial-AI-Foundation/installers_for_various_tools
cd installers_for_various_tools
python3 verus_installer_from_release.py --version "0.2025.08.25.63ab0cb"
python3 verus_analyzer_installer.py
python3 scip_installer.py

Install probe-verus:

git clone https://github.com/Beneficial-AI-Foundation/probe-verus
cd probe-verus
cargo install --path .

`create`

Initialize structure files from source analysis. Uses probe-verus tracked-csv to auto-discover exec functions with Verus specs and generate .md stub files.

verilib-cli create                  # Default structure root
verilib-cli create --root custom/path

Options:

Option	Description
`--root <path>`	Custom structure root (default: `.verilib/structure`)

Requirements:

probe-verus installed and in PATH

`atomize`

Enrich structure files with metadata from SCIP atoms.

verilib-cli atomize                 # Generate stubs.json (full pipeline)
verilib-cli atomize -s              # Also update .md files with code-name
verilib-cli atomize --atoms-only    # Only generate atoms.json (no stubs needed)

Options:

Option	Description
`-s, --update-stubs`	Update .md files with code-name
`-n, --no-probe`	Skip running probe-verus atomize and read existing atoms.json
`-c, --check-only`	Check if .md stub files match enriched stubs.json without writing
`--atoms-only`	Only generate atoms.json, skip stubs enrichment (no `create` needed)
`--rust-analyzer`	Use rust-analyzer instead of verus-analyzer for SCIP generation

Auto-detection: When no .verilib/config.json exists and the project's Cargo.toml has no Verus dependencies (vstd, verus_builtin, verus_builtin_macros, or [package.metadata.verus]), atoms-only mode is enabled automatically. This lets verilib-cli atomize work on pure Rust projects without running create first.

`specify`

Check specification status and manage spec certificates.

verilib-cli specify

This command:

Runs probe-verus specify to get spec info
Shows interactive menu for uncertified functions
Creates cert files for selected functions
Updates specified status in stubs

Options:

Option	Description
`-n, --no-probe`	Skip running probe-verus specify and read existing specs.json
`-c, --check-only`	Check if all stubs with specs have certs, error if any are missing

`verify`

Run verification and update stubs with verification status.

verilib-cli verify
verilib-cli verify --verify-only-module my_module

Options:

Option	Description
`--verify-only-module <name>`	Only verify functions in this module
`-n, --no-probe`	Skip running probe-verus verify and read existing proofs.json
`-c, --check-only`	Check if any stub has status "failure", error if any are found

API Commands

Programmatic interface for managing .verilib files. Useful for scripting and automation.

`api get`

Get metadata for a specific file.

verilib-cli api get --file example

`api list`

List all files, optionally filtered by status.

verilib-cli api list
verilib-cli api list --filter specified

`api set`

Set metadata fields for a file.

verilib-cli api set --file example --specified true

`api batch`

Batch update multiple files from JSON input.

verilib-cli api batch --input updates.json

`api create-file`

Create a new file with content from string, file, or stdin.

verilib-cli api create-file --path ./config.json --content '{"key": "value"}'
verilib-cli api create-file --path ./dest.txt --from-file ./source.txt
echo "content" | verilib-cli api create-file --path ./piped.txt

Global Options

Option	Description
`--debug`	Enable debug output
`--json`	Output in JSON format (API commands)
`--dry-run`	Show changes without applying (API commands)

verilib-cli --debug deploy

Workflows

1. User Workflow

Interactive workflow for setting up and managing verification on a project:

# Clone and setup
git clone git@github.com:Beneficial-AI-Foundation/dalek-lite.git
cd dalek-lite
git checkout -b sl/structure

# Step 1: Create structure files
# Auto-discovers exec functions with Verus specs via probe-verus
verilib-cli create

# Step 2: Run atomization
# Generates stubs.json with atom dependencies from SCIP analysis
# Updates .md files with code-name, code-path, and code-line
verilib-cli atomize --update-stubs

# Step 3: Manage specifications
# Prompts user to certify functions with changed specs
# Updates stubs.json with specification statuses
verilib-cli specify

# Step 4: Run verification
# Runs Verus verification and updates stubs.json with proof statuses
verilib-cli verify

2. CI Workflow

Non-interactive workflow for continuous integration. Uses --check-only to validate without modifications:

# Step 1: Verify structure files are up to date
# Fails if .md stub files don't match enriched stubs.json
verilib-cli atomize --check-only

# Step 2: Verify all specs are certified
# Fails if any stub with specs is missing a cert
verilib-cli specify --check-only

# Step 3: Verify no failures
# Fails if any stub has status "failure"
verilib-cli verify --check-only

3. Server Workflow

Workflow for server environments where probe-verus runs separately in job queues and Docker containers. Uses --no-probe to read from pre-generated JSON files and --check-only to validate:

# probe-verus commands run separately in Docker containers:
#   probe-verus atomize ... -o .verilib/atoms.json
#   probe-verus specify ... -o .verilib/specs.json
#   probe-verus verify ... -o .verilib/proofs.json

# Step 1: Verify structure files match atoms.json
verilib-cli atomize --no-probe --check-only

# Step 2: Verify all specs are certified from specs.json
verilib-cli specify --no-probe --check-only

# Step 3: Verify no failures from proofs.json
verilib-cli verify --no-probe --check-only

Configuration

API Key Storage

Platform	Storage Method
macOS	Keychain
Linux	File system (`~/.verilib/credentials.json`)
Windows	Windows Credential Manager

Override with environment variable:

export VERILIB_STORAGE=file    # Force file storage
export VERILIB_STORAGE=keyring # Use system keyring

Local Files

Path	Description
`.verilib/config.json`	Repository and structure configuration
`.verilib/structure/`	Structure files (`.md` with YAML frontmatter)
`.verilib/stubs.json`	Enriched stub data
`.verilib/atoms.json`	Atom metadata from probe-verus
`.verilib/certs/specs/`	Specification certificates
`.verilib/*.atom.verilib`	Code files
`.verilib/*.meta.verilib`	Metadata for code files

Troubleshooting

macOS Security Warning

If you see "Apple could not verify verilib-cli is free of malware":

Option 1: Use the installer script (recommended)

curl -sSL https://github.com/Beneficial-AI-Foundation/verilib-cli/releases/latest/download/verilib-cli-installer.sh | sh

Option 2: Remove quarantine attribute

xattr -d com.apple.quarantine /path/to/verilib-cli

Option 3: Allow in System Preferences → Security & Privacy → General

Authentication Issues

verilib-cli status    # Check status
verilib-cli auth      # Re-authenticate

Storage Issues

Force file storage if keyring fails:

export VERILIB_STORAGE=file
verilib-cli auth

Debug Mode

verilib-cli --debug init
verilib-cli --debug deploy

Development

Building from Source

git clone https://github.com/Beneficial-AI-Foundation/verilib-cli.git
cd verilib-cli
cargo build --release
cargo test
cargo install --path .

Requirements

Rust 1.70+ (2021 edition)
Git (for auto-detection)
Platform-specific keyring support (optional)

Contributing

Fork the repository
Create your feature branch (git checkout -b feature/amazing-feature)
Commit your changes (git commit -m 'Add some amazing feature')
Push to the branch (git push origin feature/amazing-feature)
Open a Pull Request

License

MIT License - see LICENSE for details.

Support

Issues - Report bugs or request features
Discussions - Ask questions or share ideas
Wiki - Additional documentation

Changelog

See CHANGELOG.md for version history.

Name		Name	Last commit message	Last commit date
Latest commit History 74 Commits
.github/workflows		.github/workflows
src		src
tests		tests
.gitignore		.gitignore
CLAUDE.md		CLAUDE.md
Cargo.lock		Cargo.lock
Cargo.toml		Cargo.toml
Dockerfile		Dockerfile
LICENSE		LICENSE
README.md		README.md
dist-workspace.toml		dist-workspace.toml
plan-dist-manifest.json		plan-dist-manifest.json

Folders and files

Latest commit

History

Repository files navigation

verilib-cli

Features

Execution Modes

Installation

One-Line Installers (Recommended)

Package Managers

Manual Installation

Quick Start

Repository Workflow

Verification Workflow

Auto-Validation for Trusted Specs

Repository Commands

auth

status

init

deploy

pull

reclone

Structure Commands

Prerequisites

create

atomize

specify

verify

API Commands

api get

api list

api set

api batch

api create-file

Global Options

Workflows

1. User Workflow

2. CI Workflow

3. Server Workflow

Configuration

API Key Storage

Local Files

Troubleshooting

macOS Security Warning

Authentication Issues

Storage Issues

Debug Mode

Development

Building from Source

Requirements

Contributing

License

Support

Changelog

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases 20

Packages 0

Uh oh!

Contributors

Uh oh!

Languages

`auth`

`status`

`init`

`deploy`

`pull`

`reclone`

`create`

`atomize`

`specify`

`verify`

`api get`

`api list`

`api set`

`api batch`

`api create-file`

Packages