Specifications, Static checkers, Runtime Assertion Checkers, and SMT-solvers — these tools can be used to make your software better. However, getting them to work together is often difficult and error-prone. Spekl is a platform for streamlining the process of authoring, installing, and using specifications and formal methods tools.
Any existing project can be used with Spekl — you can integrate Spekl into your project either via the command line, IDE, or use continuous integration.
Spekl is a community-driven effort that supports a wide-array of program verification tools including tools like OpenJML and SAW. Our repository is quickly growing and our plugin format makes it easy to author your own verification tools.
One obstacle with getting verification tools into the hands of engineers is the task of simply running the tools, configuring the SMT solvers and so on. Spekl provides a uniform interface to your verification tools which helps make sure your tools get used.
Creating "one specification to rule them all" is easier said than done. Spekl allows you to consume existing specifications, customize them, and optionally publish your specifications back to the community so that others may benefit from your hard word.