Coma as an intermediate verification language

Coma is designed as an intermediate language for the purposes of verification conditions generation. Indeed, minimality and simplicity make Coma a good IVL candidate.

Currently it is used as a backend language for verification of Rust programs in the Creusot tool.

We are also working on verifying x86-64 assembler programs using Coma.