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).
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.
Open Verification Kernel (OVK) is an open-source, solver-agnostic verification layer for AI-agent engineering workflows.
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.
Solutions to Advent of Code 2023 problems
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)
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.
🎲 Automated Sudoku solver using SAT solvers
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).
The Verification Gate for AI-Generated Tax Decisions. Deterministic tax verification layer powered by Z3 and Decimal math — sits between AI agents and execution systems. Not a calculator, not a filing platform.
Implementation and formal mathematical verification (using Z3 SMT solver) of safety-critical drone collision avoidance logic. Project includes real-time Python visualization and Manim explanations.
Deterministic FDIR (Fault Detection, Isolation & Recovery) engine for satellites. Mitigates Single Event Upsets (SEU) via formal invariant verification. Public validation module.
Add a description, image, and links to the z3-solver topic page so that developers can more easily learn about it.
To associate your repository with the z3-solver topic, visit your repo's landing page and select "manage topics."