I've been becoming more and more interested in learning formal methods and wanted to find a good project to which I could contribute. Would the development team appreciate someone adding ACSL annotations to the codebase? Are such pull requests likely to be upstreamed? I ask this because it uses comment syntax to express the specifications and some people dislike that. However, as we all know, there are solid advantages to using formal methods, such as automatic test generation and proven absence of runtime errors.