Cuanto4 Verivita

[smover]

The goal of this issue is to understand how cuanto can support Verivita.

The questions that we should try to answer are:

• How can we support the next steps of the project? What do we need to support dynamic verification/static verification/learning?
• What did we implement in Verivita (trace runner, the verifier) that should be refactored/improved/reused across projects?

We want to write an analysis to figure these questions and identify the functionalities that we want to refactor or implement from scratch in cuanto.