Welcome to [V]!

[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

As a starting point, it is first useful to understand [V]’s building blocks. To do so, we would recommend that new users start with the following pages:

• Execution Model
• [V] Statements
• Specification Variables and Macros

Specifications

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

• Behavioral Specifications
• Temporal Specifications

Tools

A number of tools either require a [V] specification as an input, or produce a [V] specification as an output. Below is a list of tools that interact with the [V] specification language:

• Eurus
• Medjai
• OrCa