ADSL - Abstract Data Store Library

Project maintained by Bocete Hosted on GitHub Pages — Theme by mattgraham

ADSL - Abstract Data Store Library

ADSL is a gem for formal verification of Ruby on Rails models. Simply include it in your Gemfile, write a few invariants (rules) about ActiveRecord data that you wish to verify (for example, that at any given moment, every Address has a User) and run rake verify!

Besides the verification algorithm, this tool includes a DSL for specifying invariants. The syntax should feel natural to any Rails user. Look at /examples.

This tool is distributed as a Ruby gem and is uploaded to It requires Z32 and Spass3 to run. Install it and give it a try!


This gem is tested on 64 bit Linux. OS-X compatibility not tested, give it a try and tell us if it works! Windows is not supported at this moment.


rake verify <options>

Or, to just observe the extracted model,

rake adsl_translate

The gem also adds an executable adsl that can be used for more fine tuned options. Use adsl --help to look at options.


Source Repository

The ADSL gem is currently hosted at github. The github web page is You can download the source using our public git clone URL:


Issues and Bug Reports

Feature requests and bug reports can be made at



Rake is available under a Lesser GPL (LGPL) license.


This software is provided “as is” and without any express or implied warranties, including, without limitation, the implied warranties of merchantibility and fitness for a particular purpose.