Provengo by the Numbers

How Provengo and the Behavioral Programming at its core compare with today's modeling, verification and testing tools, measured in peer-reviewed studies

Provengo is a tool suite for modeling, verifying, executing, and testing system behavior. At its core is Behavioral Programming (BP), a way of writing system requirements as small, independent scenarios that can be run, formally verified and used to generate tests.

Provengo is not built on a new idea. It is built on a long line of research. BP grew out of scenario-based programming, which David Harel and colleagues began developing with Live Sequence Charts around 2001. Over the past twenty years, research groups at the Weizmann Institute, Ben-Gurion University and elsewhere have published dozens of papers that developed BP's theory, its model checkers and its testing methods, and measured them against other approaches.

Provengo packages this research into user-friendly tools that engineers can use.

This extensive research is why we can back our claims with numbers. We say that:

• Provengo models are smaller than the alternatives.

• They run, and they can be formally verified.

• They are modular, so you change them by adding to them.

• Developers who are not formal-methods experts can write them.

• The same model drives automated testing and can serve as a control layer that governs AI components at runtime.

Claims like these are easy to make and hard to check. So this post compares Provengo and BP with named state-of-the-art (SotA) tools on concrete measures: model size, verification time, test effectiveness, defects found, rework, required expertise and traceability. Every number in this post comes from a peer-reviewed publication or a public preprint, listed at the end, and most of the original tables and figures are reproduced here.

The short version

Each row names the SotA baseline it is measured against, and marks whether the gain mainly affects cost, schedule or performance.

Dimension	SotA baseline	SotA	Provengo / BP	Gain	C/S/P
Model size	Petri net, level-crossing benchmark (5 tracks, with faults)	20,556 states / 157,551 transitions	975 states / 6,822 transitions	−95% / −96% (−80% on average across configurations)	Cost Schedule
Requirement addition	Petri net (Tic-Tac-Toe, one win line)	23 arcs, 2 places, 1 transition, 1 token, wired into the existing net	One ~6-line b-thread, existing code unchanged	Additive instead of invasive	Schedule
Verification time	Java PathFinder (Tic-Tac-Toe)	> 80 min	8 s	~600× faster	Schedule
Verification scale	Java PathFinder	3 threads: 511 s; 6 threads: out of memory	25 b-threads: 2.2 s; 10,000 b-threads: ~10.7 min	Orders of magnitude more concurrency	Performance
Symbolic verification	Explicit-state checking (BPpy)	398.8 s, 1.19 GB; 519K-state model times out at 60 min	3.9 s, 0.08 GB; same model in 7.4 s	~100× faster, ~15× less memory	Cost Schedule
Chance a 10-test suite catches an elusive bug	Random test selection	0.219 / 0.067	0.709 / 0.216	~3.2×	Pefrormance
Test-suite generation	Best of 1,000 random suites	561 ms (protocol), 49 s (Moodle)	39 ms, 22 s, with comparable or better coverage	2–14× faster	Schedule
Reproducing concurrency bugs	Brute-force sampling, 17 benchmark bugs	~0.13 average trigger probability	~0.53	~4×	Performance
Debugging effort	Raw failing behavior, 27 ASML industrial benchmarks	14.3 states on average	4.1 states	−71%	Schedule
Real defects found	(none known before)	—	New concurrency bug in Moodle 3.9; 2 major cart bugs in Adobe Magento	—	Performance
Rework after a defect	Edit existing model or code	Changes to existing code	0 changes; fixes are added as patch modules	Additive repair	Cost Schedule
Required expertise	Formal-methods engineer	Specialist background writes the model	An LLM writes the b-threads; undergraduates read BP models at 75–83% correctness after one lecture and an online course	+47% comprehension with BP idioms	Cost
Requirements-to-test traceability	Manual trace matrix	Manual	Automatic: one b-thread per requirement, every test and counterexample is an event trace	Automated	Cost Schedule
Cost of verification	Spin, other checkers	Translate code into the checker's language	Verify the executable model directly	No translation step	Cost

The rest of this post explains where each number comes from and what it does and does not show.

1. What we compare against

"State of the art" is only useful if it names a specific tool. We use these baselines:

• Behavior modeling: Petri nets. Petri nets are a mature, widely taught formalism for concurrent behavior. We compare against published Petri-net models of standard benchmarks rather than ones we built ourselves.

• Verifying code: Java PathFinder (JPF). JPF is NASA's model checker for Java programs. Like BP, it checks real executable code, which makes it the closest comparison in the verification & execution aspects..

• Verifying models: Spin. Spin is the most widely used explicit-state model checker. It requires the system to be re-written in its own modeling language, Promela.

• Test selection: random sampling, best-of-N search and combinatorial sequence testing (the Kuhn-Higdon sequence-covering criterion), which are what most model-based testing pipelines use today.

• Traceability: a manual requirements-to-test matrix, which is still the norm in regulated industries.

2. What a behavioral program looks like

This section is a quick intro to BP. If you are familiar with the concepts, or has taken one of the classes taught about this, you can safely skip to the next section where we start the detailed comparative analysis.

A behavioral program is a set of small, independent scenarios called b-threads. Each one describes one requirement in terms of events: what it requests, what it waits for, and what it blocks. At each step, the BP engine picks an event that some b-thread requested and no b-thread blocked.

Here are the basic rules of Tic-Tac-Toe as an executable behavioral program, each rule is a separate piece of code (b-thread):

cells.forEach(c => {
  bthread('Cells cannot be marked twice', function(){
    sync({waitFor: [O(c), X(c)]})
    sync({  block: [O(c), X(c)]})
  })
})

bthread('Enforce turns', function(){
  while(true) {
    sync({waitFor: AnyX, block: AnyO})
    sync({waitFor: AnyO, block: AnyX})
  }
})

bthread('Play randomly', function(){
  while(true)
    sync({request: XOmoves})
})

The model can be:

• run as a program,

• model-checked by exploring all orders of events,

• used to generate tests, since each run is a sequence of events that becomes a test case, and

• deployed as a supervisory layer that blocks unsafe actions at runtime.

3. Model size

In What Petri Nets Oblige Us to Say [3], we demonstrated the difference between two ways of composing behavior. In a Petri net (and also automata, statecharts, and other formalisms), all requirements are wired into one shared structure, so the modeler has to spell out how each requirement interacts with all the others. In BP, each requirement is a separate b-thread, and the BP engine handles the requirement composition automatically.

A small change to the requirements, a large change to the model

Size matters most when requirements change. The figure below is a published Petri net for Tic-Tac-Toe. It implements only two of the game's four requirements: cells cannot be marked twice, and players take turns. It specifies exactly the same behavior as the three b-threads in the above code (Section 2).

A Petri net model for the game of Tic-Tac-Toe. This model implements only two requirements out of four.

Next, we added the following requirement: the game ends when X fills the top row. This is only one case from the original requirement (in fact, the game ends when X or Y fill any row or column). Yet, as the next figure shows, the Petri-net implementation takes additional 23 arcs, 2 places, 1 transition and 1 token, all connected to the existing net:

Our Extended version of the above Petri net, now including a requirement for terminating the game when X wins by taking the first row.

In BP, we can handle the entire requirement (for all lines) with only one parameterized b-thread of about six lines, added next to the existing ones:

lines.forEach(l => {
  bthread('Detect X win', function(){
    for(let i = 0; i < 3; i++)
      sync({waitFor: [X(l.c1),X(l.c2),X(l.c3)]})
    sync({request: XWin}, 100)
    sync({  block: bp.all })
  })
})

With l = first row, this b-thread specifies the same behavior as the extended Petri net above. The lines.forEach loop creates one copy for each of the eight lines, so the other seven lines need no extra code.

Importantly, the added requirements does not require any update to existing b-threads (from Section 2). Completing the game takes two more b-threads of the same shape, one that detects a win by O and one that detects a tie:

lines.forEach(l => {
  bthread('Detect O win', function(){
    for(let i = 0; i < 3; i++)
      sync({waitFor: [O(l.c1),O(l.c2),O(l.c3)]})
    sync({request: OWin}, 100)
    sync({  block: bp.all })
  })
})

bthread('Detect a tie', function(){
  for(let i = 0; i < 9; i++)
    sync({request: Tie}, 90)
    sync({  block: bp.all })
})

Fewer states, and no hidden bugs

In the same paper, we modeled the classic level-crossing benchmark, a railway crossing with a gate and several tracks, and compared it with the published Petri-net models of the same requirements (from 1987 and 2016).

The two models differ for the same reason as in the Tic-Tac-Toe case. A Petri net obliges the modeler to spell out how every requirement interacts with all the others: how a train approaching on one track affects the gate, how the gate affects the other tracks, and what happens when a fault occurs in between. In BP, each requirement is written on its own, and the BP engine works out the interactions.

Spelling out those interactions by hand is also where mistakes hide. When we implemented the same requirements in BP and verified the published Petri nets against our model, we found that the published nets were wrong. With 2 tracks, the net allows 109 million forbidden behaviors and misses 117 million required ones. These errors had stayed hidden in the literature for decades, since the first model was published in 1987.

Below is a size comparision of each model's state space, which is what a verifier has to explore.

Track count	Petri net states	Petri net transitions	BP states	BP transitions	States removed	Transitions removed
1	10	13	5	6	50%	54%
2	83	185	13	26	84%	86%
3	483	1,532	35	101	93%	93%
4	2,434	10,110	97	372	96%	96%
5	11,304	58,327	275	1,327	98%	98%

The extra states are not the cost of a different notation. Rather, they are the undesired behaviors described above: the Petri net reaches states that the requirements forbid, and a verifier has to explore all of them.

The size difference grows with the track count. At 1 track, BP saves about half the states. At 5 tracks it saves 98%. The level-crossing benchmark also showed the same pattern as Tic-Tac-Toe: extending it from one track to several meant restructuring the Petri net, while the BP model only needed copies of existing b-threads.

Further evidence

• Theory. Harel et al. [4] proved that due to BP's request, wait-for and block idioms, in some cases, BP models are each exponentially more succinct than ordinary automata. Combined with nondeterminism and universality, the gain is triple-exponential.

• Context. In Context-Oriented BP [2], a smart-home model with 10 kitchens and 10 bathrooms needs 50 modules in plain BP and 3 in COBP, and that number stays the same as the house grows.

• Liveness. With our must-finish idiom [9], a reference solution went from 14 lines with cyclomatic complexity 7 to 6 lines with complexity 3. We also tested the idiom against Dwyer's specification patterns [15], the standard catalog of the kinds of properties engineers actually ask verifiers to check, such as "X never happens", "every request is eventually followed by a response" and "A must happen before B". Dwyer, Avrunin and Corbett built the catalog from more than 500 real specifications from industry and academia, and each pattern comes in several scopes (always, before an event, after an event, between two events). All 55 patterns map to small b-threads, including the 18 liveness patterns, which require that something good eventually happens.

4. Verification time and scale

Against Java PathFinder

Java PathFinder (JPF) checks real Java code, so it has to consider every way in which Java threads can interleave. BP's semantics only treat the synchronization points between b-threads as states, so the state space is far smaller. JPF ran out of memory at 6 threads, while BP verified 10,000 b-threads with only 402 states. [2].

Tool	Threads / b-threads	States	Time
JPF	3	438,568	511 s
JPF	6	out of memory	—
BP (BPjs)	25	27	2.2 s
BP (BPjs)	10,000	402	640 s (~10.7 min)

On Tic-Tac-Toe, JPF took more than 80 minutes and the BP model checker took 8 seconds [1].

Against Spin

Spin is the most widely used model checker for concurrent systems. Harel et al. [1], compared Spin to two BP formal model checkers on standard benchmarks from the BEEM database: dining philosophers and the bridge-crossing puzzle. To find the deadlock in 12 dining philosophers, the BP model checker visited about 11× fewer states than Spin, in similar time. For the bridge-crossing puzzle it visited 24 states instead of 96,194.

Benchmark	Spin time (s)	BP time, find deadlock (s)	BP time, deadlock-free (s)	Spin states	BP states, find deadlock	BP states, deadlock-free
4 dining philosophers	~0	0.031	0.063	80	50	80
6 dining philosophers	~0	0.063	0.172	729	528	728
12 dining philosophers	4.26	3.812	342	531,440	46,632	531,440
4 people crossing a bridge	~0	0.547	N/A	96,194	24	N/A

Two points matter more than the raw numbers. First, Spin requires the system to be re-written in Promela before it can check anything, and that translation has to be redone whenever the system changes. BP checks the same executable model that runs and generates tests. Second, a model checker that searches for counterexamples, as BP's does, is designed to find a bug quickly rather than to explore every state.

Symbolic verification

Our newer symbolic back-end for BPpy [7] cut verification of a benchmark from 398.8 s to 3.9 s and memory from 1.19 GB to 0.08 GB. A 519,151-state model that timed out after 60 minutes with explicit-state checking was verified in 7.4 s.

5. Testing and defect detection

More bugs caught by the same number of tests

Most test-generation tools offer a fixed menu of coverage criteria, such as all-pairs (two-way) coverage or Kuhn and Higdon's sequence coverage. If the bugs you are worried about do not fit one of them, the tool cannot aim at them. Provengo is not limited to such a menu. Because the space of possible tests is an executable BP model, a coverage criterion is simply a function that scores a test suite. Testers can therefore write domain-specific criteria that capture what they know about where bugs hide: the order of messages in a protocol, money moving between two accounts in a transaction, or the symmetries of a game board. The standard criteria remain available as special cases. We have also developed several ways to generate small test suites that score high on whichever criterion is chosen, including AI-based search such as the genetic algorithm described below.

In Generalized Coverage Criteria for Combinatorial Sequence Testing [10], we demonstrated the effect. In the alternating-bit protocol, bugs are typically triggered by a few events that happen back to back. So we defined a criterion that rewards covering consecutive event sequences (written Σ*wΣ*), whereas Kuhn–Higdon also credits the same events when other events occur between them. We injected four bugs and measured the probability that a 10-test suite, selected from the same model, triggers each one. Our domain-specific criterion beat both random selection and Kuhn–Higdon on all four bugs, and the gap was largest for the rare ones: about 3.2× more likely to catch the two rarest bugs than random selection (0.219 → 0.709 and 0.067 → 0.216), while Kuhn–Higdon did no better than random on them.

On Moodle, the real concurrency bug depends on three events that need not be adjacent. There, the classic Kuhn–Higdon 3-way criterion was the right fit and raised the probability of catching the bug from 0.372 (random) to 0.986, compared with 0.512 for Σ*wΣ*.

The lesson is not that one criterion is always best. The best criterion depends on the domain, and Provengo lets you pick it, or write your own, over the same model. In every case we measured, the right criterion beat random selection.

Real bugs in real software

• Moodle 3.9: a previously unknown concurrency bug [10].

• Adobe Magento: two major cart-management bugs, reported to Adobe [11].

• Published models: errors in the level-crossing Petri nets that had gone unreported for decades, including 109 million forbidden behaviors and 117 million missing required ones [3], see Section 3.

Fewer tests, same coverage

Tic-Tac-Toe has 255,168 possible games. Symmetry-based coverage classes reduce that to 26,830 (−89%). With Provengo, adding one constraint as a single new story, with no change to existing code, cut a generated suite from 1,064 to 165 tests [11].

Making intermittent bugs reproducible

Concurrency bugs are hard to fix because they rarely show up. In Black-Box Bug Amplification for Multithreaded Software [12], part of our testing toolchain, we search for the test inputs that make such bugs most likely to appear. Across 17 concurrency benchmarks, we measured how likely the best test each method found is to trigger the bug, as a function of how many tests the method may try. Our ensemble method reaches about 0.53 within 500 tests. Brute-force sampling reaches only about 0.13 after 3,900.

Method	100 tests	500 tests	1,500 tests	2,500 tests	3,900 tests
Ensemble (ours)	0.43	0.53	0.53	0.53	0.53
Genetic algorithm	0.10	0.13	0.14	0.15	0.15
Brute-force sampling	0.01	0.03	0.07	0.11	0.13
Simulated annealing	0.01	0.01	0.03	0.04	0.04

Average probability that the best test found triggers the bug. Values are read from the paper's Figure 5 and rounded to two decimals [12].

Shorter debugging

When a check fails, an engineer has to understand why. On 27 industrial lithography-control benchmarks from ASML (RERS 2019), our learned failure explanations shrank what the engineer has to read from 14.3 states to 4.1 on average (−71%), and in the largest case from 37 states to 4 [13].

6. Rework and the Schedule

Rework is a highly frustrating and time-consuming activity. When a late requirement or a defect forces changes to a model that other parts depend on, every one of those parts has to be re-reviewed, re-verified and re-tested. That is what moves delivery dates and contract milestones.

BP is designed so that changes are added rather than edited in:

• New requirements are new b-threads. Section 3 showed the difference: one new rule in a Petri net touches dozens of existing arcs, while in BP it is one new module.

• Repairs are new b-threads too. In Non-Intrusive Repair of Safety and Liveness Violations [5], model-checker counterexamples were automatically turned into readable patch b-threads, with zero changes to existing code. Tic-Tac-Toe was fully repaired with 26 generated patches. A deadlock reported from the field was patched in 0.5 s to 45 min, depending on the case.

• Re-verification is automatic. The patched model is checked by the same tool, with no translation step, so making a change and verifying it happen together.

7. Requirements from many disciplines, and the cost of verifying them

Real systems collect requirements from safety engineers, operators, domain experts, regulators and software teams. In most toolchains, someone has to merge them into one model, written in one formalism, usually by a formal-methods specialist. This merge is where much of the cost of verification goes, and it is repeated every time any discipline changes its requirements.

BP avoids the merge:

• Each discipline writes its own b-threads. The safety engineer writes "never open the valve while pressure is above X" as one scenario. The operator writes the startup procedure as another. BP's semantics combine them, and the model checker finds any conflicts between them.

• One requirement, one module, one trace. Every counterexample and generated test is a sequence of events that points directly to the b-threads, and so to the requirements, involved. Traceability comes from the model's structure and does not need a separate matrix.

• No translation step. Tools such as Spin require translating the system into the checker's own language. BP verifies the model that runs and generates the tests, so the expensive and error-prone step of keeping two models in sync disappears.

• Different languages, one model. BP has been implemented in JavaScript (BPjs, Provengo), Python (BPpy), Java and other languages. Because the semantics are shared, scenarios written by different teams can be combined into one model.

8. Who can use it

One of the main barriers to formal methods has been that they need specialists to write and read the models. With BP, that barrier has largely disappeared.

Today, an LLM writes the model. Each b-thread is a short piece of ordinary JavaScript that captures one requirement, which is exactly the kind of code that large language models write well. Engineers give the requirements to an LLM, get b-threads back, and run, verify and test them in Provengo right away. Anything the LLM gets wrong shows up as a counterexample from the model checker or a failing test, before it reaches the system.

People still review the model, and non-specialists can do this with BP . Our comprehension studies measured whether people without a formal methods background can read a BP model and judge whether it reflects an intent .

• 49 third-year undergraduates, after a single 90-minute session, answered 47% more comprehension questions correctly with our structured BP idioms than without them (10.91 vs. 7.41 of 16, p < 0.001). On preemptive abort, they scored about 6× higher [14].

• 109 undergraduates, after one lecture and the Provengo online course, reached 75–83% correctness reading BP models [8].

• 93 first-year students, after a short video, wrote correct BP models for 70–85% of basic tasks. With our liveness idiom, 82% correctly judged whether a liveness requirement could be achieved, compared with 44% without it [9].

These are students, not practicing engineers, and they had hours of training rather than weeks. The people who usually do formal methods have years of specialist background. If students can check a BP model after a lecture, an engineer can check the b-threads an LLM wrote from their requirements.

9. Governing AI agents

The same rules that verify a system can supervise it at runtime. In Enhancing Deep Learning with Scenario-Based Override Rules [6], BP rules running on top of deep-reinforcement-learning controllers, an Internet congestion controller and a navigation robot, reduced collisions and raised success rates with no retraining, over 100 runs per agent. Using deep RL to find a valid execution of a BP model took 15–20s regardless of problem size, while explicit synthesis grew from 123s to 927s [7].

This is how BP can act as a governance layer for AI: the agent proposes actions, the b-threads block what the requirements forbid, and the same b-threads can be model-checked and tested before deployment.

10. What we have not measured yet

Being clear about the gaps matters as much as reporting the gains:

• Modeling time in hours. The numbers here measure model size and comprehension. We do not yet have a controlled study that measures hours to build the same model in BP and in an SotA tool.

• Coverage percentages in industrial deployments. Our coverage results come from benchmarks and open-source systems. Industrial pilot data is the next step.

• Practicing engineers. The expertise studies used students. A study with industry engineers is planned.

• LLM-written models. In our own work, LLMs routinely develop large and complex BP models. We have not yet measured this systematically, for example how accurate LLM-generated b-threads are or how long engineers take to review them.

We are collecting these numbers in ongoing pilots with Provengo customers and will publish them here.

Sources

1. D. Harel, R. Lampert, A. Marron, and G. Weiss, "Model-checking behavioral programs," in Proceedings of the 9th ACM International Conference on Embedded Software (EMSOFT), Taipei, Taiwan, 2011, pages 279–288. LINK

2. A. Elyasaf, "Context-oriented behavioral programming," Information and Software Technology, volume 133, Article number 106504, May 2021. LINK

3. A. Elyasaf, T. Yaacov, and G. Weiss, "What Petri nets oblige us to say: Comparing approaches for behavior composition," IEEE Transactions on Software Engineering, volume 49, number 4, pages 2303–2317, April 2023. LINK

4. D. Harel, G. Katz, R. Lampert, A. Marron, and G. Weiss, "On the succinctness of idioms for concurrent programming," in Proceedings of the 26th International Conference on Concurrency Theory (CONCUR), Leibniz International Proceedings in Informatics (LIPIcs), volume 42, 2015, pages 85–99. LINK

5. D. Harel, G. Katz, A. Marron, and G. Weiss, "Non-intrusive repair of safety and liveness violations in reactive programs," in Transactions on Computational Collective Intelligence XVI, Lecture Notes in Computer Science, volume 8780, 2014, pages 1–33. LINK

6. A. Ashrov and G. Katz, "Enhancing deep learning with scenario-based override rules: A case study," in Proceedings of the 11th International Conference on Model-Based Software and Systems Engineering (MODELSWARD), 2023, pages 253–268. LINK (arXiv preprint)

7. T. Yaacov, G. Weiss, A. Ashrov, G. Katz, and J. Zisser, "Exploring and evaluating interplays of BPpy with deep reinforcement learning and formal methods," in Proceedings of the 20th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), 2025, pages 27–40. LINK

8. A. Ashrov, A. Sturm, A. Elyasaf, and G. Katz, "A study on the comprehensibility of behavioral programming variants," in Proceedings of the 20th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), 2025, pages 252–267. LINK

9. T. Yaacov, A. Elyasaf, and G. Weiss, "Adding liveness to behavioral programming: Theory, implementation, and user study," Requirements Engineering, volume 30, number 2, pages 149–171, June 2025. LINK

10. A. Elyasaf, E. Farchi, O. Margalit, G. Weiss, and Y. Weiss, "Generalized coverage criteria for combinatorial sequence testing," IEEE Transactions on Software Engineering, volume 49, number 8, pages 4023–4034, August 2023. LINK

11. M. Bar-Sinai, A. Elyasaf, G. Weiss, and Y. Weiss, "Provengo: A tool suite for scenario driven model-based testing," in Proceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2023, pages 2062–2065. LINK (arXiv preprint)

12. Y. Weiss, G. Amram, A. Elyasaf, E. Farchi, O. Margalit, and G. Weiss, "Black-box bug amplification for multithreaded software," Mathematics, volume 13, number 18, Article number 2921, September 2025. LINK

13. T. Yaacov, G. Weiss, G. Amram, and A. Hayoun, "Automata models for effective bug pattern description," in Proceedings of the ACM/IEEE 28th International Conference on Model Driven Engineering Languages and Systems (MODELS), 2025, pages 119–129. LINK (arXiv preprint)

14. A. Ashrov, M. Gordon, A. Marron, A. Sturm, and G. Weiss, "Structured behavioral programming idioms," in Enterprise, Business-Process and Information Systems Modeling, Lecture Notes in Business Information Processing, 2017, pages 319–333. LINK

15. M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, "Patterns in property specifications for finite-state verification," in Proceedings of the 21st International Conference on Software Engineering (ICSE), 1999, pages 411–420. LINK