OxiZ is a high-performance Satisfiability Modulo Theories (SMT) solver written entirely in Rust. This project is part of an initiative to reimplement Z3 in Pure Rust. Pure Rust is a fundamental requirement - no C/C++ dependencies, no FFI bindings, just clean, safe Rust code.
IIT Madras OpenMP (IMOP) compiler framework is an open-source, source-to-source, OpenMP-aware compiler for OpenMP (and serial) C programs.
Mimi language: contract-verified systems programming with LLVM codegen, Z3 verification, and structured concurrency
Minesweeper3D è un'implementazione tridimensionale del classico gioco, sviluppato utilizzando la libreria Ursina in Python. Il gioco presenta una griglia di cubi 3D, alcuni dei quali contengono mine. L'obiettivo è rivelare tutti i cubi che non contengono mine, utilizzando i numeri sui cubi rivelati come indizi sul numero di mine adiacenti.
Learner-Verifier Framework for formal synthesis of Control Barrier Functions (CBF).
This repository features AI-based game projects (Tic-tac-toe, Checkers, Sudoku solver) developed as part of the CS 235 course (optional).
A Python-based predictor using z3 to reverse-engineer and predict random values generated by Math.random in V8 with 100% accuracy. This script leverages a series of Math.random() values (min 5) to deduce future states.
Neuro-symbolic RL agent that learns to pentest networks it has never seen — GPT-4o compiles CVE preconditions into a Z3 action mask over a GraphSAGE PPO policy. Zero-shot attack-graph transfer, negatives disclosed.
Deterministic verification layer for infrastructure as code. Verifies AWS IAM policies, network reachability, and cost estimates before deployment — sits between AI agents and cloud execution. Powered by Z3 and NetworkX.
Sovereign, provider-agnostic, and local-first 3-tier agentic OS powered by the 14-axis Mnemosyne memory architecture, formal verification, and secure local-hybrid routing.
Proof-based physics gate for LLM outputs — every rejection is a Z3 proof, every uncertainty is an abstention
Open Verification Kernel (OVK) is an open-source, solver-agnostic verification layer for AI-agent engineering workflows.
Use z3 to predict Math.random() output for V8, Chrome, Firefox, and Safari
Graph visualizer and planning tool for courses at the University of Toronto.
Solutions to Advent of Code 2023 problems
Hospital shift scheduling, 20 ways: backtracking, SAT/SMT, flow, annealing, and more — head-to-head on 1,036 instances.
Repositório dos trabalhos de casa da UC de Métodos Formais em Engenharia de Software (MFES) - Mestrado em Engenharia Informática (MEI/MIEI) - Universidade do Minho (UMinho)
A SAT-based framework for computing Envy-Free and Pareto-Efficient Virtual Machine Allocation in Cloud Federation using the Z3 Solver and Counterexample-Guided Abstraction Refinement (CEGAR).
NeSy-DocAI: Neuro-Symbolic Document AI Research Engine for Auditable Financial Invoice Parsing (System 1 Vision + System 2 Z3 SMT Solver)
🎲 Automated python Sudoku solver using SAT solvers
To associate your repository with the z3-solver topic, visit your repo's landing page and select "manage topics."