verify
Formally verifies the specification, searching for safety and liveness violations.
Description
This sub-command performs a depth-first search (DFS) over the entire specification space, looking for violations of halt(message) statements (safety violations) and non-progress cycles (liveness violations). verify is exhaustive up to --max-depth: if a violation exists within that depth, verify will find it.
When violations are found (up to 10), verify writes an HTML report describing each one, including a counter-example trace: the sequence of events leading to the violation. Additionally, Provengo will exit with error code 1, so that CIs and agents can easily detect that a violation was found.
Safety Violations
A safety violation means that "something irreversibly bad" happens at on of the runs possible under the model. Consider a loan request processor, for example. Assume that a regulation prevents giving an underage person a loan. We can capture this requirement and verify against it using the following bthread:
bthread("No loans for under-age", function(){
waitForAll( IS_CHILD_EVENT, LOAN_GRANTED ); (1)
halt("Regulatory violation: we just gave a loan to a child."); (2)
});-
Waits for the events marking that the a applicant is a child, and a loan being granted. The order of the events does not matter.
-
Marks the run as having a safety violations, with human readable explanation of what the violation is.
Liveness Violations
Intuitively, a liveness violation is a run where something that must happen at some point never does. For example, a loan process that runs - possibly forever - without concluding whether the loan request is approved or rejected. More formally, a liveness violation is a reachable cycle in the specification’s state space in which some goal you require to recur is never met.
For example, the requirement "we should keep seeing a heartbeat event", verified against a BP model where a cycle exists that loops forever without ever producing such event, would generate a liveness violation.
A liveness requirement is expressed by marking a sync() call as hot: a b-thread that is "hot" at a given sync point is asserting that it must not remain stuck at that exact sync forever.
bthread("Expect a HEARTBEAT, again and again", function () {
while (true) {
sync({ waitFor: Event("HEARTBEAT") }, undefined, true); // isHot=true
}
});The Constraints library provides a non-blocking alternative with a somewhat nicer syntax. Note that this examples is not equivalent: it only requests that the RESET event would happen at least once, at some point in the future:
bthread("Expect a HEARTBEAT at some point", function () {
Constraints.requires(Event("HEARTBEAT")).eventually();
});If verify's DFS finds a reachable cycle in which this b-thread is hot at every point, it reports a liveness violation naming the b-thread and the cycle. In the HTML report, liveness violations get a liveness tag (instead of safety), and their counter-example trace highlights where the offending cycle starts and, for cycles longer than one step, where it loops back around.
This checks two flavors of hot-cycle by default: a single b-thread that’s hot throughout the whole cycle, and a b-thread still hot when the b-program ends.
Deadlocks
verify also checks for deadlocks by default — a state where some event is requested but every b-thread that could otherwise let it through is blocking it, so no event can legally be selected and the b-program is stuck. This needs no configuration; deadlocks found during the DFS are reported alongside safety and liveness violations, tagged deadlock in the HTML report.
Parameters
--max-depth NUM-
Maximum DFS exploration depth. Defaults to the same value as
analyze's--max-depth. --random-seed NUM-
Seed number for random number generation.
-o/--output-file PATH-
Path to a directory where the verification report should be created.
--offline-
Creates a report that does not use on-line resources. Increases file size, but allows full functionality in offline environments.
The below modle has a subtle bug - it allows withdrowals from an empty bank account:
bthread("Choose transaction", function () {
while (true) {
request([bp.Event("DEPOSIT", { amount: 10 }), bp.Event("WITHDRAW", { amount: 10 })]);
}
});
bthread("Balance must never go negative", function () {
let balance = 0;
while (true) {
let e = waitFor(any(/^(DEPOSIT|WITHDRAW)$/));
if (e.name === "DEPOSIT") {
balance += e.data.amount;
} else {
balance -= e.data.amount;
if ( balance >= 0 ) {
halt("Balance went negative: " + balance);
}
}
}
});provengo verify finds the violation and writes an HTML report listing the violation’s description and a counter-example trace of events that leads to a negative balance (e.g. [DEPOSIT → DEPOSIT → WITHDRAW → WITHDRAW → WITHDRAW] ). Each event in the trace can be expanded to see its data, and a "Show All Details" button toggles all events at once.
The following model causes a liveness violation:
bthread("Emit TICK forever", function () {
while (true) {
request(bp.Event("TICK"));
}
});
bthread("Expect a RESET, again and again", function () {
while (true) {
sync({ waitFor: bp.Event("RESET") }, undefined, true); // hot: must eventually happen
}
});Nothing ever requests RESET, so the reachable cycle where only TICK repeats never satisfies the "Expect a RESET" b-thread’s goal. Running provengo verify again finds this too: a violation tagged liveness, described as Hot run violation: b-threads {Expect a RESET, again and again} can each get to an infinite hot loop…, with its trace marking the step where the bad cycle starts.
See also: analyze, which visualizes the specification space rather than searching it for violations.