Do you know any teams that are actually trying to build implementations of this?
We are currently in contact with some companies that are interested in developing off-chain protocols. Unfortunately, currently we do not have the resources to do a full-fledged implementation but we are happy to contribute to them by, e.g., writing formal specifications, proving security of protocols, etc. This is also where our main expertise lies. That said, for the basic virtual payment channels, we made a highly non-optimized prototype implementation of the contracts in Solidity. The main purpose of this implementation was to estimate gas costs. Here is the link: GitHub - PerunEthereum/Perun: Implementation of the Perun protocol.
In principle, I personally am satisfied that it’s fundamentally possible to achieve all of the things that you claim in the way that you’re doing it; the risk of error that worries me is closer to the implementation side (both smart contract code and daemon logic).
Our modeling currently is at the abstract specification level only. This means it deals with logic errors due to, e.g., concurrency (which can be very tricky to get right) and also the composition of complex protocols. In fact, one of the main features of our modeling approach is that it enables us to give a rather modular specification and not one monolithic protocol that simultaneously has to deal with the vast number of special cases.
Of course, as you said our long term vision is to have fully verified code (hopefully even machine-checked) and reference implementations of the smart contracts and daemon logic. Before we move to this step however we first need to get the underlying protocol specification right – which turned out to be quite complex for these protocols. Indeed during the design we figured out many technical subtleties that we would not have noticed without a proof-driven design approach.
Such a bottom-up approach where we start with abstract protocol specification and then move to low level implementation is quite common in (cryptographic) protocol design. For instance, currently a “hot topic” in protocol design is to get fully-verified implementations of TLS. Also, there part of the process is to get the abstract protocol specification right and to find a modular design such that fully automated verification can be applied. We believe that one approach to designing secure off-chain protocols (payment/state channel networks, plasma, etc.) is to follow a similar path as these attempts.