Usability and Accessibility of Formal Modeling and Verification Software

Aartifact Lightweight Verification System and Related Frameworks

From 2008 until 2013, this research effort undertaken at Boston University investigated, prototyped, and evaluated (within the classroom and for domain-specific use cases) features and techniques that could improve the usability and accessibility of formal modeling and verification software tools and services. It included the development of variants of a verification system called Aartifact, focusing on the use of heuristic algorithms, fact databases, interactive interfaces, and browser compatibility. Related and/or interoperable frameworks for visualization of mathematical concepts and mathematical content management and presentation were also developed as part of this work and peripheral efforts.

Software Prototypes and Frameworks

  • Aartifact Verification System.
    A Haskell implementation of a formal verification system that can leverage a database of formal facts and an ensemble of heuristic symbolic search algorithms to verify mathematical proofs assembled in a human-legible style and level of detail.
  • Aartifact Light Web-Based Verifier.
    A browser-compatible lightweight variant of the Aartifact Verification System implemented using JavaScript.
  • Sheaf and Protoql.
    Early versions of the Sheaf framework for web-based presentation of mathematical content and the Protoql visualization library were developed as part of this effort. This included the integration of the Aartifact Light interactive proof environment directly into the assignment sections of course notes written and presented using Sheaf, as well as the embedding of Protoql interactive visualizations into the same Sheaf course notes.

Publications and Reports


This effort benefitted from the support and cooperation of Boston University, including the Department of Computer Science, the Hariri Institute for Computing.

This work was partially supported by the National Science Foundation under Grants #0720604, #0735974, #0820138, #0952145, and #1012798. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.