What Can I Contribute?

What Can I Contribute?

We are building a community of contributors. Please contact us to join the community!

Who can help?

We are looking for anyone with interest in making software safer and more secure. We need people who can read code. If you have experience using logic, that’s great but not essential.

What kind of contributions are of interest?

Annotated Software

Our main goal is to accumulate annotated versions of APIs that are in common use, so contributing in this way is most beneficial to the project.

More annotations will give static analysis tools more information, so they will be able to provide a more thorough analysis. Ideally, such material becomes a part of the released software for that API. Where that is not possible, we will host such material on our GitHub project site.

Use Cases

If you are creating or checking annotated source code yourself, we are interested in your experience. As appropriate, we will post a summary of your experience with a given tool, piece of software, or annotation language on this site.

Tools and Languages

If you know of annotation languages or tools that process annotations+source code that we have not mentioned on this site, please tell us about them. There are many theorem provers and model checkers that have their own input languages but have no connection to source code, and those are not our main interest. Rather, we are focused on tools that read both (such as Frama-C, Spec#, or the JML tools) or ones that have converters (like SPIN) that translates source code into the tool’s modeling language. Send us an email with links to relevant material and we’ll add it to our public information.


This project will evolve over time. Your feedback on what works and what doesn't is very welcome.


The NSF requires that material produced under this project be made openly available. All independent material originated by this project per se will be licensed under the Apache 2 license. Annotations that are modifications of existing source files will likely need to be made available under the same license as the original source code. Contributions from contributors will be accepted with any OSI-approved license, though we would prefer an Apache-2 or BSD 2-Clause license.