H2 was an experimental specification language for hardware interfaces and so on ...
It was built on the HPR L/S (aka Orangepath) library.
HPR L/S uses an heirarchy of abstract machines. Each machine is a database of declarations, executable code and goals. The goals are assertions about the system behaviour, input directly, or generated from compilation of temporal logic and data conservation rules into automata. Executable code can pass through the system unchanged, but any undriven internal nodes are provided with driver code that ensures the system meets its goals.
Example output prime example.
Example output data src and sink using a channel.
Example output data transfer over an interface using imperative code to describe the protocol.
Example output synthesis of a P2P connection using a joining automaton.
BVCI Transactors, Monitors and Bus Bridges Definition and Synthesis.
UIA Processor Use and Synthesis.