Skip to content

v0.8.1 - Exhaustive verification at scale

Choose a tag to compare

@ssweber ssweber released this 04 May 19:55
· 8 commits to main since this release
62be332

prove() and pyrung lock now handle industrial-scale programs.

The prove() and pyrung lock shipped in v0.7.0 worked on tutorial-sized programs but hit Intractable
on anything resembling a real PLC project. This release rewrites the state-space explorer, validated against a new examples/packml_bench.py — a 17-state PackML machine with indirect block lookups, task sequencing, and an alarm historian.

Single-flip BFS, a pre-BFS elision pipeline, accumulator absorption, and a blockless compiled kernel
combine to make exhaustive verification practical at industrial scale. Lock files now project to
lock=True tags, omit False values, resolve choice labels, and support band predicates for collapsing
numeric outputs into categories. Python 3.12 minimum.

Migration note: TagMap now auto-stamps external=True on input-mapped tags and lock=True on
output-mapped tags, so most programs need no changes. If you're not using TagMap, mark any tag whose
value comes from outside the ladder as external=True — without it, the verifier treats it as internal
state and won't vary it.

Not a certified verification tool

prove() is a best-effort exhaustive check — it catches real bugs and is useful for development
confidence, but it is not a safety-rated formal proof. Do not use it as a substitute for proper functional
safety processes (IEC 61508, ISO 13849, etc.) on machinery that can hurt people.