Verifier Support Matrix

The following tables present which features of Verifier should be considered fully, partially, or un- supported, following this guide:

• ✅: Fully supported
• ⚠️: Fully supported within listed limitations
• 🚧: In progress, some features may not work and documentation may be unclear
• ❌: Unsupported

Interoperability Features

Transports

Transport	Verifier in Tangram Pro	Verifier in CI
ActiveMQ	✅	✅
HTTP	❌	❌
Kafka	✅	✅
MQTT	✅	✅
NATS	✅	✅
RabbitMQ	✅	✅
ZeroMQ	✅	✅
TCP	❌	✅
UDP	❌	✅

Serializers

Transport	Verifier in Tangram Pro	Verifier in CI
CSV	✅	✅
Direct (Binary)	✅	✅
JSON	✅	✅
LMCP	✅	✅
MAVLink	✅	✅
OMS 2.0 (XML)	✅	✅
Protobuf	✅	✅
ROS	✅	✅
STANAG 4586	✅	✅
WOSA	✅	✅
XML	✅	✅

Flex Features

The Flex language has a large surface area, not all of which is currently supported by Verifier. These tables help disambiguate Verifier's current support for features of the Flex language.

Declarations

Declaration	Supported
Imports	🚧
Message	✅
Struct	✅
Variant	✅
Enum	⚠️ ONLY int32 base
type	✅
newtype	❌
Global protocol	❌
Local protocol	✅
Component	✅
System	❌
Connection	✅

Annotations

Annotation	Supported
@Topic(name: string)	✅
@End(term: string)	✅
@Heartbeat(frequency: string, jitter: string)	✅
@Timeout(duration: string)	✅
@Delay(min: string, max: string)	✅
@MinDelay(min: string)	✅
@MaxDelay(max: string)	✅

NOTE: Annotations must be defined at top of Flex file. See any of the annotation details below for examples of usage.

Time strings: The @Heartbeat, @Timeout, @Delay, @MinDelay, and @MaxDelay annotations accept time strings — a number followed by a unit suffix. The suffixes ms (milliseconds) and s (seconds) are accepted by all of them, and hz (hertz) is accepted only by the @Heartbeat frequency. Decimals are allowed (e.g. "0.5s", "1.5hz"). Verifier logs a warning for any non-zero value below 100ms, as such short intervals are unlikely to be reliable over a network transport.

Topic Annotation

For transports which use Publish/Subscribe models with topics, the @Topic annotation tells Verifier which topic a message should be sent or received on. Topics which aren't listed in any protocol will not be watched, and messages which arrive on the incorrect topic will be marked invalid.

All annotations which are placed on send or recv statements must be placed at the end of the expression, just before the closing ;.

annotation Topic(name: string)

component Test;
component Other;

local protocol basicFlow in Test {
    recv let msg1: RequestNumber
        from Other
        @Topic("messages.RequestNumber");

    send let msg2: GiveNumber
        where msg2.id == msg1.id
        to Other
        @Topic("messages.GiveNumber");
}

End Annotation

@End specifies the conditions on which Verifier should mark a protocol as completed, after all sends and recvs have occured. The value for this annotation can be any one of:

• Exit - The component program should exit before the protocol can succeed
• Timeout - Verifier should wait for a message timeout after receiving all messages (program exit would result in an error)
• ExitOrTimeout - Either of the above conditions is considered successful
• LastMessage - The protocol is considered successful after the last specified send or recv occurs

annotation End(term: string)

@End("LastMessage")
local protocol basicFlow in Test {
    recv let msg1: RequestNumber
        from Other;

    send let msg2: GiveNumber
        where msg2.id == msg1.id
        to Other;
}

Heartbeat Annotation

@Heartbeat marks a local protocol as a repeating heartbeat. Rather than running once and finalizing, the protocol loops for the entire duration of the test run: each time its send/recv statements complete, Verifier records the cycle's verdict and immediately restarts the protocol to begin the next cycle. This is useful for validating periodic messages such as keep-alives, status pings, or sensor updates. If any cycle fails, the heartbeat protocol fails.

@Heartbeat is placed on the local protocol declaration, like @End. It takes two arguments:

• frequency - The expected interval between messages. Accepts ms, s, or hz.
• jitter (optional) - The allowed timing variation around the frequency. Accepts ms or s, and must be less than the frequency. If omitted, it defaults to 10% of the frequency.

Each cycle is given an effective timeout of frequency + jitter, so a message is expected within that window. Note that an explicit @Timeout on a heartbeat protocol is ignored — the frequency + jitter window always governs per-cycle timing.

Heartbeat protocols are validated concurrently while a normal (non-heartbeat) protocol is under test; they do not run on their own. You may define multiple heartbeats (e.g. at different frequencies) alongside your normal protocols.

annotation Heartbeat(frequency: string, jitter: string)

@Heartbeat("1s", "200ms")
local protocol pingBeat in Test {
    send any Ping to Other;
}

Timeout Annotation

@Timeout overrides the global Message Timeout for a single protocol. Verifier considers the protocol timed out if no relevant message arrives within this duration (measured from the last accepted message). Use it when one protocol needs more (or less) time than the rest of your test.

@Timeout is placed on the local protocol declaration and takes a single time string (ms or s).

annotation Timeout(duration: string)

@Timeout("500ms")
local protocol P in Edge {
    send let dataOut: SensorData
        to Server;

    recv let dataIn: GatheredData
        from Server;
}

Delay, MinDelay, and MaxDelay Annotations

These three annotations tell Verifier to defer delivering a message that the component is waiting to recv, simulating a slow or delayed sender. When a recv is annotated with a delay, Verifier waits a random duration within the configured window before generating and sending the message.

They are placed at the end of a recv statement, just before the closing ; (like @Topic):

• @Delay(min, max) - Delay by a random time in the range [min, max]. Requires both arguments, and min must be less than max.
• @MinDelay(min) - Set only the lower bound. The upper bound defaults to the protocol's effective timeout.
• @MaxDelay(max) - Set only the upper bound. The lower bound defaults to 0.

@Delay cannot be combined with @MinDelay or @MaxDelay on the same recv. To specify both bounds, either use @Delay(min, max) or pair @MinDelay with @MaxDelay.

The delay is capped at the protocol's effective timeout, so be sure to set a large enough @Timeout (or global Message Timeout) to accommodate the delay — otherwise Verifier warns that the message may never arrive in time.

annotation End(term: string)
annotation Delay(min: string, max: string)
annotation Timeout(duration: string)

@End("LastMessage")
@Timeout("5000ms")
local protocol delayedFlow in Test {
    recv let msg1: RequestNumber
        from Other
        @Delay("2000ms", "2400ms");

    send let msg2: GiveNumber
        where msg2.id == msg1.id && msg2.other == msg1.other
        to Other;
}

To specify only one bound, use @MinDelay or @MaxDelay instead:

annotation MinDelay(min: string)
annotation MaxDelay(max: string)
annotation Timeout(duration: string)

@Timeout("5000ms")
local protocol oneSidedFlow in Test {
    // Waits at least 200ms (upper bound defaults to the protocol timeout)
    recv let slow: RequestNumber
        from Other
        @MinDelay("200ms");

    // Waits between 0 and 3s
    recv let bounded: RequestNumber
        from Other
        @MaxDelay("3s");
}

Protocol Features

Protocol Feature	Supported
All primitive types (message fields)	✅
All primitive types (protocol variables)	✅
Built-in Functions	🚧
send let	✅
send any	✅
send ... where { ... }	✅
send <var>	⚠️ See linked example for limitations
recv let	✅
recv any	✅
listen	🚧
branch	🚧
loop	❌
do	🚧

Constraints

Constraints should be specified as a list of boolean checks.

See the examples below as well as in the Flex protocol examples.

The table below shows the current limitations of Verifier with respect to the larger capability list of Flex protocols.

Why are some features supported in send but not recv?

Verifier acts as the reciprocal of the component: when the component protocol sends a message, Verifier receives it, and when the component recvs a message, Verifier has to generate and send it.

Generating a message from constraints is a difficult task. We continue to add new features to our message generators, so please keep an eye on the supported constraint types shown in this table.

Type & Variable Features

Feature	send	recv
Single var conditional statements
Non-array primitive types	✅	✅ Full support for boolean operations
Array/List primitive types	✅	⚠️ arr_field == [] and length(arr_field) == x only
Variant type matching	✅	❌
Enum type matching	✅	✅ Full support for boolean operations
Dependency on prior message	✅	✅
Dependency on variable	✅	✅
Multi var conditional statements	✅	❌

Flex Std Lib Features

The Flex Standard Library supports a large number of functions & operators. The below table shows support for standard library features specifically in send and recv constraint clauses (i.e. assuming and where). The list of std lib features supported by Verifier is constantly growing:

Std Lib Feature	send	recv
Literals/Primitive Types	⚠️ Custom length (u)intN aren't supported, only standard lengths (8, 16, 32, 64)	⚠️
Built-in Functions	⚠️ Currently, only length is supported for lists as shown in Type & Variable Features	⚠️
Custom function definitions	✅	❌
transform definitions	❌	❌
match	✅	❌
assert	❌	❌
for	❌	❌
scan/fold/try/filter	❌	❌
Operators	✅	⚠️ Bitwise & bit shift operators are not supported

Examples

Primitive Type Constraints

Valid Single Variable Boolean Expressions

enum DataType int32 {
    Temperature = 0;
    WindSpeed   = 1;
    AirPressure = 2;
    Rainfall    = 3;
}

struct DataRequest {
    id: string;
    time: uint64;
    request: DataType;
}

struct DataRespone {
    id: string;
    time: uint64;
    response: RequestType;
    data: float64;
}

component Dashboard;
component WeatherStation;

local protocol Example in Dashboard {
    send let req: DataRequest
        where req.id == "weatherstation_0"
            && req.time > 0
            && req.request == DataType.Rainfall
        to WeatherStation;

    recv let res: DataRespone
        assuming res.id == "weatherstation_0"
            && res.time >= req.time
            && res.response == req.request
        from WeatherStation;
}

List Constraints

Valid Constraints

local protocol X in Component {
    recv let first: MsgOne
        assuming length(first.array_field) == 10
        from Other;

    recv let second: MsgTwo
        assuming second.array_field == [1, 2, 3, 4, 5]
        from Other;
}

Invalid Single Variable Array Index Expressions

local protocol X in Component {
    recv let msg: Msg
        // Verifier does not support indexing constraints
        assuming msg.array_field[0] == 10
        from Other;
}

Invalid Multi-Variable Boolean Expressions

message struct Position {
    lat: float64;
    long: float64;
}

component A;
component B;

local protocol X in A {
    // Verifier will struggle to generate the message which the component says it must receive
    recv let pos: Position
        assuming pos.x + pos.y < 100
        to B;
}

send Constraints

message struct Position {
	lat: float64;
	long: float64;
}

component Component;
component Other;

local protocol X in Component {
    // WRONG: Message blocks are _not_ checked as constraints
    send Position {
            lat = 10,
            long = 20
        }
        to Other;

    // RIGHT: Instead, do:
    send let pos: Position
        where pos.lat == 10
           && pos.long == 20
        to Other;
}