The Eldarica model checker

A monad for interfacing with external SMT solvers

A Formal Method playground for limboole, Z3, nuXmv, Alloy, and Spectra

A parser and some utils for SMTLIB. For a fully compliant parser, see https://github.com/Gbury/dolmen/.

Run Z3 entirely in your browser using WebAssembly

In this project, we have automated the synthesis of loop invariants for a for a very small programming language. It converts SMT-Lib files into SMT2

Semantic-Based Worst Case Execution Time of Loop-Free C Programs using Optimization Modulo Theory

Parse smt2 in Haskell

Explorations in Uniform Sampling of SMT2 Constraints

VUT FIT v Brne IZLO project 2

SMTLIB2 bindings for FSharp

Analysis of Formal Specifications SAT, SMT, Alloy, NuSMV.