Overview

[V] is a declarative specification language for communicating tests/properties with the Veridise infrastructure. It provides a language- and blockchain-agnostic method of specifying properties about smart contracts.

Getting Started

First, we provide a guide for learning [V] by example:

• Hello, Bugs!
• Intro to LTL
• Aggregate Properties
• Guiding the Search

Building Blocks of [V]

The following pages describe how [V] works at a high-level, starting with the execution model the language assumes before describing the general structure of [V] specifications.

• Execution Model
• [V] Statements
• Specification Variables

Specifications

[V] supports several different types of specifications that can be used to perform different tasks. Currently we support the following types of specifications:

• Invariant Specifications
• Temporal Specifications

Complete Language

For a more complete description of all language features in [V], see the following page(s):

• Language Description