Formal verification for Tapio v1.5 model

[azat-hafizov]

Create a formal model as part of Tapio v1.5 tech paper This issue is dependent on the following list (but not limited to):

• [x] #21
• [x] #28
• [x] #25