unpackdev/solgo

Solidity parser in Go, designed to transform Solidity code into a structured format for enhanced analysis, particularly beneficial for developers using Go to analyze Solidity smart contracts.

Language: Go - Size: 155 MB - Last synced: about 5 hours ago - Pushed: about 6 hours ago - Stars: 21 - Forks: 4

ranea/CASCADA

A tool to evaluate the security of cryptographic primitives against distinguishing attacks with bit-vector SMT solvers.

Language: Python - Size: 4.07 MB - Last synced: about 6 hours ago - Pushed: about 7 hours ago - Stars: 26 - Forks: 8

plus3-labs/o1js-merkle

Merkle Tree for o1js (membership / non-membership merkle witness) with Pluggable Storage

Language: TypeScript - Size: 770 KB - Last synced: about 9 hours ago - Pushed: about 9 hours ago - Stars: 7 - Forks: 2

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs

Language: HTML - Size: 139 MB - Last synced: about 8 hours ago - Pushed: about 9 hours ago - Stars: 346 - Forks: 48

prove-rs/z3.rs

Rust bindings for the Z3 solver.

Language: Rust - Size: 582 KB - Last synced: 1 day ago - Pushed: 2 days ago - Stars: 315 - Forks: 102

jiahaoxiang2000/sbox-bgc

use the smt solver to find the sbox implementation

Language: Jupyter Notebook - Size: 290 KB - Last synced: 1 day ago - Pushed: 2 days ago - Stars: 0 - Forks: 0

VeriFIT/z3-noodler Fork of Z3Prover/z3

The Z3-Noodler String Solver

Language: C++ - Size: 122 MB - Last synced: 2 days ago - Pushed: 3 days ago - Stars: 4 - Forks: 5

AliveToolkit/alive2

Automatic verification of LLVM optimizations

Language: C++ - Size: 5.98 MB - Last synced: 2 days ago - Pushed: 3 days ago - Stars: 695 - Forks: 87

ucsd-progsys/liquidhaskell

Liquid Types For Haskell

Language: Haskell - Size: 56.4 MB - Last synced: 3 days ago - Pushed: 3 days ago - Stars: 1,153 - Forks: 130

cleanunicorn/karl

Monitor smart contracts deployed on blockchain and test against vulnerabilities with Mythril. It was presented at DEFCON 2019.

Language: Python - Size: 4.3 MB - Last synced: 3 days ago - Pushed: 3 days ago - Stars: 312 - Forks: 79

py2many/py2many

Transpiler of Python to many other languages

Language: Python - Size: 1.73 MB - Last synced: 1 day ago - Pushed: about 2 months ago - Stars: 603 - Forks: 46

JohnLyu2/z3alpha

Z3alpha synthesizes efficient Z3 strategies tailored to your problem set! Repo for the IJCAI'24 paper: Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis.

Language: Python - Size: 6.55 MB - Last synced: 3 days ago - Pushed: 3 days ago - Stars: 3 - Forks: 0

LampicJ15/Kafka-Connect-Transforms

Language: Java - Size: 1.56 MB - Last synced: 4 days ago - Pushed: over 1 year ago - Stars: 0 - Forks: 1

nam20485/OdbDesign

A free open source cross-platform C++ library for parsing ODB++ Design archives, accessing their data, and building net list product models. Exposed via a REST API packaged inside of a Docker image.

Language: C++ - Size: 2.58 MB - Last synced: 3 days ago - Pushed: 4 days ago - Stars: 20 - Forks: 9

ufmg-smite/lean-smt

Tactics for discharging Lean goals into SMT solvers.

Language: Lean - Size: 535 KB - Last synced: 6 days ago - Pushed: 6 days ago - Stars: 68 - Forks: 16

Squiddleton/Megaten

An unofficial collection of standardized data from the Shin Megami Tensei and Persona games

Language: TypeScript - Size: 130 MB - Last synced: 2 days ago - Pushed: 6 days ago - Stars: 14 - Forks: 3

trailofbits/manticore

Symbolic execution tool

Language: Python - Size: 43.5 MB - Last synced: 6 days ago - Pushed: 8 months ago - Stars: 3,645 - Forks: 468

sosy-lab/java-smt

JavaSMT - Unified Java API for SMT solvers.

Language: Java - Size: 123 MB - Last synced: about 20 hours ago - Pushed: about 21 hours ago - Stars: 171 - Forks: 42

LeventErkok/sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

Language: Haskell - Size: 16.2 MB - Last synced: 7 days ago - Pushed: 8 days ago - Stars: 233 - Forks: 32

pathawks/sudoku-smt

Exploring SMT solvers by solving Sudoku puzzles

Language: C - Size: 108 KB - Last synced: 10 days ago - Pushed: about 6 years ago - Stars: 0 - Forks: 0

ModelWriter/smtlib-tool

Eclipse-based SMTLIB Editor

Language: Python - Size: 138 MB - Last synced: 15 days ago - Pushed: about 5 years ago - Stars: 0 - Forks: 0

yaqwsx/jlcparts

Better parametric search for components available for JLC PCB assembly

Language: JavaScript - Size: 542 MB - Last synced: 18 days ago - Pushed: 19 days ago - Stars: 491 - Forks: 46

max-prosper/stringify-json-smt

Kafka Connect SMT to convert values to JSON strings

Language: Java - Size: 33.2 KB - Last synced: 11 days ago - Pushed: over 2 years ago - Stars: 6 - Forks: 3

informalsystems/apalache

APALACHE: symbolic model checker for TLA+ and Quint

Language: Scala - Size: 57.9 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 403 - Forks: 38

oeb25/smtlib-rs

A high-level API for interacting with SMT solvers.

Language: Rust - Size: 283 KB - Last synced: 17 days ago - Pushed: 17 days ago - Stars: 16 - Forks: 6

akiomik/smt1-note

真・女神転生 (Shin Megami Tensei) の日本語版SFCについてのデータをまとめています。

Language: Scala - Size: 5.58 MB - Last synced: 18 days ago - Pushed: about 1 month ago - Stars: 5 - Forks: 0

classicwuhao/uran

uran: A small engine for creating formulas accepted by SMT solver.

Language: Java - Size: 73.8 MB - Last synced: 21 days ago - Pushed: 21 days ago - Stars: 3 - Forks: 1

jenkinsci/mailer-plugin

This plugin allows you to configure email notifications for build results

Language: Java - Size: 649 KB - Last synced: 14 days ago - Pushed: 14 days ago - Stars: 35 - Forks: 106

seanpm2001/SNU_2D_ProgrammingTools_IDE_SMT

The SMT Programming language IDE submodule for SNU Programming Tools (2D Mode)

Language: SMT - Size: 418 KB - Last synced: 22 days ago - Pushed: over 1 year ago - Stars: 2 - Forks: 2

seanpm2001/Learn-SMT

A repository for showcasing my knowledge of the SMT programming language, and continuing to learn the language

Language: SMT - Size: 378 KB - Last synced: 22 days ago - Pushed: over 1 year ago - Stars: 3 - Forks: 1

al8n/lsmtree

Sparse Merkle tree for a key-value map.

Language: Rust - Size: 124 KB - Last synced: 17 days ago - Pushed: almost 2 years ago - Stars: 18 - Forks: 1

uuverifiers/princess

The Princess Theorem Prover

Language: Scala - Size: 52.1 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 18 - Forks: 5

minor-industries/reflow-oven

Basic reflow oven for SMT soldering

Language: Go - Size: 31.3 KB - Last synced: 25 days ago - Pushed: 26 days ago - Stars: 1 - Forks: 0

UnitTestBot/ksmt

Kotlin/Java API for various SMT solvers

Language: Kotlin - Size: 172 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 27 - Forks: 12

EladLeev/KeyToField-smt

A Kafka Connect Single Message Transform (SMT) that enables you to append the record key to the value as a named field

Language: Java - Size: 46.9 KB - Last synced: 28 days ago - Pushed: 28 days ago - Stars: 16 - Forks: 0

cwi-swat/allealle

AlleAlle: a Bounded Relational Model Finder with Data

Language: Rascal - Size: 864 KB - Last synced: 29 days ago - Pushed: over 2 years ago - Stars: 4 - Forks: 1

hydra/pnpconvert

SMT Pick and Place conversion utility

Language: Groovy - Size: 643 KB - Last synced: 18 days ago - Pushed: about 1 month ago - Stars: 8 - Forks: 2

imandra-ai/batsmt

[wip] Modular SMT solver in rust

Language: SMT - Size: 660 KB - Last synced: 30 days ago - Pushed: over 3 years ago - Stars: 10 - Forks: 1

imandra-ai/abstract-transition-systems

[alpha] An implementation of several classic transition systems that describe algorithms for SAT or SMT, for interactive exploration

Language: OCaml - Size: 229 KB - Last synced: 30 days ago - Pushed: about 2 years ago - Stars: 1 - Forks: 1

imandra-ai/batsmt-ocaml

OCaml bindings for batsmt

Language: Rust - Size: 94.7 KB - Last synced: 30 days ago - Pushed: about 5 years ago - Stars: 3 - Forks: 0

c-cube/mc2

[research] A modular SMT solver in OCaml, based on mcSAT

Language: SMT - Size: 9.08 MB - Last synced: 30 days ago - Pushed: 5 months ago - Stars: 38 - Forks: 5

AD1024/Sager

A Demonic Graph Synthesizer

Language: Racket - Size: 24.2 MB - Last synced: about 1 month ago - Pushed: over 4 years ago - Stars: 4 - Forks: 0

lsrcz/grisette

A monadic library for symbolic evaluation

Language: Haskell - Size: 1.91 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 44 - Forks: 3

sberbanker/kafka-connect-rgs-custom-ops Fork of cjmatta/kafka-connect-insert-uuid

Трансформации для Kafka Connect | Kafka Connect SMTs

Language: Java - Size: 54.7 KB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 1 - Forks: 0

SemanticMediaWiki/SemanticMetaTags

Allows to generate HTML <meta> elements from semantic annotations

Language: PHP - Size: 182 KB - Last synced: about 1 month ago - Pushed: about 2 months ago - Stars: 12 - Forks: 6

rindPHI/isla

The ISLa (Input Specification Language) language & solver.

Language: Python - Size: 27.3 MB - Last synced: 28 days ago - Pushed: about 1 month ago - Stars: 53 - Forks: 4

viperproject/axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).

Language: SMT - Size: 94.4 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 2 - Forks: 2

TendTo/dlinear

Refactor of dLinear4 https://github.com/martinjos/dlinear4

Language: C++ - Size: 9.96 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 1 - Forks: 0

FStarLang/FStar

A Proof-oriented Programming Language

Language: F* - Size: 725 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 2,558 - Forks: 231

deut-erium/RNGeesus

SMT based attacks on non cryptographic PRNGs

Language: Python - Size: 1.32 MB - Last synced: 28 days ago - Pushed: about 1 year ago - Stars: 56 - Forks: 2

valpackett/unshift 📦

Reverses bitwise operations using CVC4 to find individual components of bitmasks

Size: 0 Bytes - Last synced: about 1 month ago - Pushed: about 1 year ago - Stars: 1 - Forks: 0

philzook58/z3_tutorial

Jupyter notebooks for tutorial on the Z3 SMT solver

Language: Jupyter Notebook - Size: 1.19 MB - Last synced: 18 days ago - Pushed: 7 months ago - Stars: 147 - Forks: 19

shaowei-cai-group/z3pp

Language: C++ - Size: 6.17 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 38 - Forks: 7

SUSE/doc-smt-11

Official SUSE Linux Enterprise Subscription Management Tool Documentation

Size: 855 KB - Last synced: about 1 month ago - Pushed: almost 3 years ago - Stars: 2 - Forks: 3

cedoor/sparse-merkle-tree

Sparse Merkle tree implementation in TypeScript.

Language: TypeScript - Size: 707 KB - Last synced: 2 days ago - Pushed: about 3 years ago - Stars: 20 - Forks: 3

ucsd-progsys/live

Slides for talk on Language-Integrated Verification

Language: JavaScript - Size: 53.3 MB - Last synced: about 2 months ago - Pushed: over 6 years ago - Stars: 0 - Forks: 0

stp/stp

Simple Theorem Prover, an efficient SMT solver for bitvectors

Language: C++ - Size: 33.1 MB - Last synced: about 2 months ago - Pushed: 5 months ago - Stars: 482 - Forks: 129

yangky11/smt-portfolio

A simple wrapper to run multiple SMT solvers in parallel

Language: Python - Size: 17.6 KB - Last synced: 21 days ago - Pushed: 5 months ago - Stars: 4 - Forks: 0

pysmt/pysmt

pySMT: A library for SMT formulae manipulation and solving

Language: Python - Size: 4.53 MB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 547 - Forks: 124

ec-m/BachelorsThesis

Mutation-based Validation of Temporal Logic Specifications with Guarantees

Size: 730 KB - Last synced: 2 months ago - Pushed: about 7 years ago - Stars: 1 - Forks: 0

smackers/smack

SMACK Software Verifier and Verification Toolchain

Language: C - Size: 7.62 MB - Last synced: about 2 months ago - Pushed: 8 months ago - Stars: 422 - Forks: 81

celestiaorg/smt 📦

A Go library that implements a Sparse Merkle tree for a key-value map.

Language: Go - Size: 176 KB - Last synced: about 2 months ago - Pushed: about 1 year ago - Stars: 136 - Forks: 52

jomorlier/IA_CNRS_ICA

Notebooks and Data for ICA's course on IA

Language: Jupyter Notebook - Size: 31 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 2 - Forks: 2

caterinaurban/Typpete

Language: Python - Size: 1.09 MB - Last synced: 28 days ago - Pushed: over 4 years ago - Stars: 33 - Forks: 6

Eseb/corpus-cleaner

Natural-language corpus cleaning scripts

Language: Python - Size: 23.4 KB - Last synced: 3 months ago - Pushed: about 8 years ago - Stars: 9 - Forks: 0

LeventErkok/sbvPlugin

Formally prove properties of Haskell programs using SBV/SMT.

Language: Haskell - Size: 542 KB - Last synced: 2 days ago - Pushed: about 2 months ago - Stars: 44 - Forks: 7

HarvardPL/formulog

Datalog with support for SMT queries and first-order functional programming

Language: Java - Size: 2.85 MB - Last synced: 3 months ago - Pushed: 7 months ago - Stars: 140 - Forks: 8

hengxin/sat-smt-satisfying

SAT and SMT

Language: Jupyter Notebook - Size: 86.2 MB - Last synced: 26 days ago - Pushed: 10 months ago - Stars: 3 - Forks: 2

testsmt/yinyang

A fuzzing framework for SMT solvers

Language: Python - Size: 3.03 MB - Last synced: 3 months ago - Pushed: 10 months ago - Stars: 173 - Forks: 21

Scheggetta/vehicle-routing-problem Fork of NglQ/vehicle-routing-problem

Multiple combinatorial optimization techniques applied to the VRP problem

Size: 1.54 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 0 - Forks: 0

markusbrammer/z3-dotnet

My attempt at understanding the Z3 API for .NET (F#)

Size: 7.81 KB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 0 - Forks: 0

sambayless/monosat

MonoSAT - An SMT solver for Monotonic Theories

Language: C++ - Size: 43.4 MB - Last synced: 2 months ago - Pushed: about 1 year ago - Stars: 105 - Forks: 32

haskell-github-trust/smt2-parser

Parse smt2 in Haskell

Language: Haskell - Size: 78.1 KB - Last synced: 2 months ago - Pushed: over 1 year ago - Stars: 1 - Forks: 1

filipeom/queries

SMT Query Dataset

Size: 4.27 MB - Last synced: 14 days ago - Pushed: 3 months ago - Stars: 0 - Forks: 0

Practical-Formal-Methods/storm

A blackbox mutational fuzzer for detecting critical bugs in SMT solvers

Language: SMT - Size: 445 KB - Last synced: 26 days ago - Pushed: over 3 years ago - Stars: 86 - Forks: 11

philzook58/z3-rise4fun Fork of bramvdbogaerde/z3-wasm

Z3 tutorials from the rise4fun website

Language: JavaScript - Size: 11.4 MB - Last synced: 18 days ago - Pushed: almost 2 years ago - Stars: 9 - Forks: 3

IagoAbal/haskell-z3

Haskell bindings to Microsoft's Z3 API (unofficial).

Language: Haskell - Size: 824 KB - Last synced: 23 days ago - Pushed: 3 months ago - Stars: 57 - Forks: 44

TyGuS/suslik

Synthesis of Heap-Manipulating Programs from Separation Logic

Language: Scala - Size: 8.07 MB - Last synced: 4 months ago - Pushed: about 1 year ago - Stars: 121 - Forks: 19

ucsd-progsys/intro-refinement-types

Introductory Tutorial on Refinement Types

Language: JavaScript - Size: 41.9 MB - Last synced: 26 days ago - Pushed: almost 3 years ago - Stars: 8 - Forks: 1

giladreich/angr_ctf Fork of jakespringer/angr_ctf

Angr CTFs covering topics from basics to intermediate.

Language: Python - Size: 3.29 MB - Last synced: 4 months ago - Pushed: over 2 years ago - Stars: 9 - Forks: 2

0xOsiris/Mev_Book

An aggregate of MEV resources, libraries, research papers, and strategies.

Size: 92.8 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 230 - Forks: 42

marcluque/YASER

Yet Another Sat solvER

Language: C - Size: 23.9 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 3 - Forks: 0

rmitache/OpenConfigurator

Open source product configuration based on visual feature models and Z3 SMT solver for providing solutions

Language: JavaScript - Size: 2.83 MB - Last synced: 4 months ago - Pushed: over 1 year ago - Stars: 10 - Forks: 1

frizensami/nus-timetable-optimizer

Codebase for the NUS Timetable Optimizer, a tool to help students at the National University of Singapore optimize their timetables to their liking.

Language: JavaScript - Size: 12 MB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 18 - Forks: 4

will-leeson/sibyl

An adaptive, Graph Neural Network Based solver selector for SMT queries

Language: Python - Size: 1.29 GB - Last synced: 5 months ago - Pushed: 6 months ago - Stars: 3 - Forks: 0

giuseppe-tanzi/CombinatorialVLSI Fork of PallottaEnrico/CombinatorialVLSI

VLSI Optimization tackles the 2-D Strip Packing Problem for Very Large Scale Integration, minimizing plate height while placing rectangular circuits without overlap. It offers versatile solutions using Constraint Programming, SAT, SMT, and ILP, with options for rotation and visualization

Language: Python - Size: 10.1 MB - Last synced: 4 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

an0r0c/kafka-connect-transform-tojsonstring

transform-to-json-string is a Single Message Transformation (SMT) for Apache Kafka® Connect to convert a given Connect Record to a single JSON String. It's an UNOFFICIAL community project.

Language: Java - Size: 87.9 KB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 26 - Forks: 11

seanpm2001/AI2001_Category-Source_Code-SC-SMT

🧠️🖥️2️⃣️0️⃣️0️⃣️1️⃣️💾️📜️ The sourceCode:SMT category for AI2001, containing SMT programming language datasets

Language: R - Size: 2.46 MB - Last synced: 22 days ago - Pushed: 6 months ago - Stars: 2 - Forks: 1

hpgrahsl/kryptonite-for-kafka

Kryptonite for Kafka is a client-side 🔒 field level 🔓 cryptography library for Apache Kafka® offering a Kafka Connect SMT, ksqlDB UDFs, and a standalone HTTP API service. It's an ! UNOFFICIAL ! community project

Language: Java - Size: 165 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 77 - Forks: 6

louisabraham/mcSATan

A diabolic implementation of mcSAT 😈

Language: Python - Size: 45.9 KB - Last synced: about 1 month ago - Pushed: almost 3 years ago - Stars: 11 - Forks: 2

Robbepop/stevia

A simple (unfinished) SMT solver for QF_ABV.

Language: Rust - Size: 1.38 MB - Last synced: 3 months ago - Pushed: about 5 years ago - Stars: 31 - Forks: 3

egk696/SimpleSMTScheduler

A simple SMT-based schedule generator for cyclic executives of real-time tasks

Language: Python - Size: 3.11 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 9 - Forks: 1

Targoman/TargomanSMT

Targoman SMT framework source code

Language: C++ - Size: 3.06 MB - Last synced: 29 days ago - Pushed: over 6 years ago - Stars: 30 - Forks: 6

touist/touist

TouIST, the IDE & Language for Logic (backed by SAT, SMT and QBF solvers)

Language: OCaml - Size: 12.1 MB - Last synced: 18 days ago - Pushed: over 3 years ago - Stars: 65 - Forks: 12

iocomp-org/iocomp

I/O server framework to enable abstracted I/O back-ends while giving capability to map seperate processes as dedicated I/O servers.

Language: C - Size: 2.09 MB - Last synced: 24 days ago - Pushed: 3 months ago - Stars: 1 - Forks: 0

nicolasAmat/SMPT

SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

Language: Python - Size: 8.91 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 25 - Forks: 4

chansey97/clprosette-miniKanren

CLP(Rosette) on top of miniKanren

Language: Racket - Size: 2.83 MB - Last synced: 7 months ago - Pushed: about 2 years ago - Stars: 8 - Forks: 0

SpoonLabs/nopol

Automatic program repair system for Java based on dynamic analysis and code synthesis with SMT. Also contains the code of Dynamoth.

Language: Java - Size: 303 MB - Last synced: 7 months ago - Pushed: about 1 year ago - Stars: 86 - Forks: 43

MachSMT/MachSMT

MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers

Language: Python - Size: 1.47 GB - Last synced: 8 months ago - Pushed: about 1 year ago - Stars: 10 - Forks: 4

konnov/bymc

Byzantine model checker

Language: C - Size: 8.13 MB - Last synced: 7 months ago - Pushed: about 1 year ago - Stars: 19 - Forks: 5