We have a way to write traditional SFGs as string diagrams and an isomorphism to behaviours which respects the kind of graphical reasoning used in the blog. So

We have a way to write traditional SFGs as string diagrams and an isomorphism to behaviours which respects the kind of graphical reasoning used in the blog. So you can show that two SFGs are behaviourally equivalent, or, using some more recent work, that all the behaviours of one are also behaviours of another, i.e. inclusion of sets of behaviours. String diagrams are also more general than SFGs, but can still be mapped to behaviours, so you could have an "unimplementable" string diagram to serve as a specification, and use the axiomatisation of inclusion to show that a particular SFG is a valid implementation of that spec. As for whether anyone outside the research programme is actually doing that, I don't know. But in principle it's a useful formal methods type theory.