StainlessVerification framework and tool for higher-order Scala programs
Alive2Automatic verification of LLVM optimizations
ApalacheAPALACHE: symbolic model checker for TLA+
FstarA Proof-oriented Programming Language
BoolectorA Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
TritonTriton is a Dynamic Binary Analysis (DBA) framework. It provides internal components like a Dynamic Symbolic Execution (DSE) engine, a dynamic taint engine, AST representations of the x86, x86-64, ARM32 and AArch64 Instructions Set Architecture (ISA), SMT simplification passes, an SMT solver interface and, the last but not least, Python bindings.
SbvSMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
JlcpartsBetter parametric search for components available for JLC PCB assembly
Mbed Hdkmbed HDK - This repository is not being maintained. For the latest updates, please use: https://github.com/ARMmbed/mbed-HDK-Eagle-Projects
DeepblockchainsDeep Blockchains - reference implementation of Plasma, Stark, SMT and more
Java SmtJavaSMT - Unified Java API for SMT solvers.
StormA blackbox mutational fuzzer for detecting critical bugs in SMT solvers
NopolAutomatic program repair and patch generation system for Java based on dynamic analysis and code synthesis with SMT, developed at University of Lille and Inria, France.
Dreal4SMT Solver for Nonlinear Theories of Reals
Cvc4CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
PysmtpySMT: A library for SMT formulae manipulation and solving
StpSimple Theorem Prover, an efficient SMT solver for bitvectors
SmackSMACK Software Verifier and Verification Toolchain
smtA Go library that implements a Sparse Merkle tree for a key-value map.
kafka-connect-transform-kryptoniteKryptonite for Kafka is a client-side 🔒 field level 🔓 crypto library for Apache Kafka® currently focused on Kafka Connect scenarios. It's an ! UNOFFICIAL ! community project
archsatA proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
z3 tutorialJupyter notebooks for tutorial on the Z3 SMT solver
vim-smt2A VIM plugin that adds support for the SMT-LIB2 format (including Z3's extensions)
suslikSynthesis of Heap-Manipulating Programs from Separation Logic
haskell-z3Haskell bindings to Microsoft's Z3 API (unofficial).
py2manyTranspiler of Python to many other languages
mailer-pluginThis plugin allows you to configure email notifications for build results
the-thoralf-pluginThis a type-checker plugin to rule all type checker plugins involving type-equality reasoning using smt solvers.
steviaA simple (unfinished) SMT solver for QF_ABV.
scalognoprototyping logic programming in Scala