Benchmarks

The Lambda distribution ships a collection of 448 safety-verification problems for parameterized systems, in benchs/collection/. Each comes with its original source next to a VMT-LIB translation, so the encoding can always be checked against what it was derived from. The file manifest.csv records, for each benchmark, its family, origin, theory and expected verdict.

Family	Instances	Origin	Theories	Safe	Unsafe	Unknown
`mcmt`	269	the MCMT distribution and its data-aware BPM models	Int, Real	184	72	13
`ivy`	60	Ivy benchmarks of IC3PO and the DuoAI protocols	none	52	0	8
`mypyvy`	62	the mypyvy examples	none	21	11	30
`misc`	57	IC3PO examples, railway systems, enumerated sorts, Suzuki–Kasami, new Ivy models	none, Int, Real	29	19	9
total	448			286	102	60

By theory, 155 benchmarks use no arithmetic, 226 use integers and 67 use reals. The expected verdict is unknown when it is not declared by the source and not established by the available tools.

The protocol families cover the usual distributed-algorithms corpus (Paxos variants, consensus, leader election, cache coherence, mutual exclusion), and the MCMT family adds arithmetic-heavy models that are less common elsewhere. Where possible, the collection also contains the inputs for other tools: mypyvy (.pyv), IC3PO (ic3po-vmt/) and DuoAI (duoai-src/).