Hi, the ATM is mega simplified, we tried modelling the entire machine and it not easy. But we are quite convinced it is possible, but it demands features from the language that we have not implemented yet tho.

Error handling is not really a problem, in fact, a lot of the time is spend thinking hard about each and every error that can occur and modelling it out ~ making sure the machine behaves well.

Problems are rather about machine synchronisation and how processes communicate (or rather, can we autogenerate proofs about their behaviour under communication).

thanks for the comments