Verum

Verum (for Verifiable Ruby Machines) is an experimental Ruby library that allows the implementation of Finite-State Machines (FSM) which are both executable and formally verifiable. The same program that controls the behavior of the machine’s actual execution is used to define the necessary features for formal verification. Verification is achieved by translating the machines into timed-automata specifications for the UPPAAL model checker. Furthermore, the machines can be visualized using the DOT format, through tools such as Graphviz.

An industrial case study using this technology has been published here:

Paulo Salem. Practical Programming, Validation and Verification with Finite-State Machines: a Library and its Industrial Application. In: Proceedings of the 38th International Conference on Software Engineering Companion. ACM, 2016. http://dl.acm.org/citation.cfm?id=2889226