Proof of Concept to help choosing a proof assistant to formalize ReAna-SPL.
The main theorem proved in Coq is in ReliabilityModels/Annotative.v (definitions and lemmas to support Annotative Probabilistic Models).
For PVS, it is a TCC (type-correctness condition) in annotative_reliability_models.pvs.