verification¶
Verification tools for distributed systems: runtime invariant checking, structured counterexample generation, CTL temporal logic model checking, and probabilistic verification (DTMC).
Verification tools for distributed systems.
This module provides: - Runtime invariant checking and state transition monitoring - Structured counterexample generation for refinement/equivalence failures - CTL temporal logic model checking - Probabilistic verification (DTMC reachability, steady-state, expected steps)
Submodules¶
| Module | Description |
|---|---|
invariant_checker |
Runtime state assertions, transition monitoring, violation tracking |
counterexamples |
Structured counterexample generation for refinement/equivalence failures |
temporal |
CTL formula AST and backward fixpoint model checking |
probabilistic |
DTMC reachability, steady-state distribution, expected steps |