SMTscope automatically analyses and visualises SMT solver execution traces.
-
Updated
Dec 10, 2025 - Rust
#
z3
Here are 50 public repositories matching this topic...
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.
-
Updated
Sep 22, 2026 - Rust
AI-Native Formal Specification Language — a bounded model checker (Lark + Z3) built for LLM write/verify/repair loops.
python verification refinement z3 model-checking formal-methods bounded-model-checking formal-specification llm
-
Updated
Sep 17, 2026 - Rust
EVM contract auditing via symbolic execution and Z3
-
Updated
Apr 16, 2026 - Rust
A bounded model checker for an IMP-style imperative language.
-
Updated
Feb 23, 2019 - Rust
Contract-first AI-native language. Write what it should do. AI proves it does.
-
Updated
Sep 20, 2026 - Rust
A tutorial on the basics of Rust Z3 API
-
Updated
Oct 13, 2022 - Rust
Statically-typed compiled language for safety-critical embedded systems — Z3-verified contracts, no_std runtime, self-healing live blocks. Ships to Cortex-M, RISC-V, and bare metal.
programming-language rust real-time embedded cortex-m compiler embedded-systems language-design z3 smt formal-verification no-std self-healing safety-critical embedded-rust
-
Updated
Sep 22, 2026 - Rust
⚖️ A simple tool for calculating the optimal number of shares to buy to maintain a proportional portfolio
-
Updated
Aug 13, 2023 - Rust
A formally verified, high-performance distributed ownership system in Rust. Features Raft consensus, SMT-based invariant checking (Z3), and safety-critical lease management.
rust distributed-systems high-performance raft consensus grpc z3 smt-solver formal-verification safety-critical distributed-locking ownership-management
-
Updated
Jan 17, 2026 - Rust
A systems language that compiles to readable C — zero-heap memory model, constant-time indexing for secret data, and Z3-verified compile-time assertions. Written in Rust.
-
Updated
Sep 12, 2026 - Rust
A symbolic executor for the QBE intermediate language
-
Updated
Jun 1, 2023 - Rust
Active Inference with ternary {-1,0,+1} actions: generative models, variational Bayes, expected free energy minimization
-
Updated
Jul 12, 2026 - Rust
A research framework for SMT-based vulnerability discovery, algebraic fault analysis, and formal verification of ML-KEM lattices.
rust cryptanalysis reverse-engineering cybersecurity z3 formal-methods algebraic-geometry post-quantum-cryptography smt-solver vulnerability-research
-
Updated
May 12, 2026 - Rust
Ternary gradient descent: straight-through estimator, ternary Adam/SGD optimizers, gradient clipping in trit space, cosine LR scheduling
-
Updated
Jul 12, 2026 - Rust
Ternary min-heap priority queue: 3 children per node, O(log₃ n) push/pop, merge, decrease-key
-
Updated
Jul 12, 2026 - Rust
Add this topic to your repo
To associate your repository with the z3 topic, visit your repo's landing page and select "manage topics."