Spekl is a Tool for Making Better Software

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.

Download Spekl (Windows, Linux, & Mac)

Spekl Documentation · Spekl in About 5 Minutes · Spekl Recipes

Easily Create New Verification Projects

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.

Install and Use Sophisticated Program Verification Tools

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.

Easily Configure and Run Checks

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.

Author and Consume Specifications

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.