We present Coma , a formally defined intermediate verification language. Specification annotations in Coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths. We define a verification condition procedure for Coma and prove its correctness. For programs with a specification given in a traditional way, with an abstraction barrier at the function boundary, our verification conditions are similar to those produced by a classical weakest-precondition calculus. For programs where abstraction barriers are put in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. Moreover, our procedure can factorize selected subgoals on the fly, which leads to more compact verification conditions. We illustrate the use of Coma on two non-trivial examples, formalized and verified using our implementation: a second-order regular expression engine and a sorting algorithm written in unstructured assembly code.

@article{paperbot3950,
  title = {<scp>Coma</scp>
                    , an Intermediate Verification Language with Explicit Abstraction Barriers},
  author = {Andrei Paskevich and Paul Patault and Jean-Christophe Filliâtre},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {48},
  number = {3},
  year = {2026},
  doi = {10.1145/3816735}
}