An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
☆400May 27, 2026Updated 5 months ago
Alternatives and similar repositories for awesome-rust-formalized-reasoning
Users that are interested in awesome-rust-formalized-reasoning are comparing it to the libraries listed below. We may earn a commission when you buy through links labeled 'Ad' on this page.
Sorting:
- Creusot helps you prove your Rust code is correct.☆1,943Updated this week
- CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.☆705Aug 20, 2026Updated 2 months ago
- Refinement Types for Rust☆931Updated this week
- A style guide for Coq☆18Nov 30, 2021Updated 4 years ago
- A collaborative bibliography of papers related to property-based testing☆37Oct 14, 2026Updated 2 weeks ago
- Deploy to Railway using AI coding agents - Free Credits Offer • AdUse Claude Code, Codex, OpenCode, and more. Autonomous software development now has the infrastructure to match with Railway.
- A static verifier for Rust, based on the Viper verification infrastructure.☆1,822Updated this week
- A model checker for Rust programs.☆3,596Updated this week
- Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.☆1,185Updated this week
- a model of MIR and the Rust type/trait system☆370Updated this week
- Verified Rust for low-level systems code☆3,478Updated this week
- A Rust verification tool☆488Oct 21, 2026Updated last week
- A verification toolchain for Rust programs☆1,099Updated this week
- An implementation and definition of the Rust trait system using a PROLOG-like logic solver☆2,022Oct 12, 2026Updated 2 weeks ago
- Analyze Rust crates without touching compiler internals☆458Updated this week
- GPU virtual machines on DigitalOcean Gradient AI • AdGet to production fast with high-performance AMD and NVIDIA GPUs you can spin up in seconds. The definition of operational simplicity.
- A precise specification for "Rust lite / MIR plus"☆1,014Jul 27, 2026Updated 3 months ago
- Logic programming in Rust☆592Aug 29, 2026Updated last month
- Rust mid-level IR Abstract Interpreter☆1,009Aug 22, 2024Updated 2 years ago
- RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.☆286Feb 12, 2022Updated 4 years ago
- Crucible is a library for symbolic simulation of imperative programs☆780Oct 19, 2026Updated last week
- A gently curated list of companies using verification formal methods in industry☆613Feb 26, 2026Updated 8 months ago
- A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.☆839May 14, 2026Updated 5 months ago
- Repository where I'll collect some demos of proof assistants that I show to various people in order to spread the magic☆38Jan 10, 2023Updated 3 years ago
- Tricks you wish the Coq manual told you [maintainer=@tchajed]☆555May 28, 2025Updated last year
- Managed hosting for WordPress and PHP on Cloudways • AdManaged hosting for WordPress, Magento, Laravel, or PHP apps, on multiple cloud providers. Deploy in minutes on Cloudways by DigitalOcean.
- Connection provers in Rust☆14Mar 13, 2024Updated 2 years ago
- Metamath Zero specification language☆422Sep 30, 2026Updated 3 weeks ago
- A framework for smart contract verification in Coq☆129Aug 25, 2026Updated 2 months ago
- ☆22Feb 10, 2022Updated 4 years ago
- egg is a flexible, high-performance e-graph library☆1,856Sep 28, 2026Updated last month
- Flowistry is an IDE plugin for Rust that helps you focus on relevant code.☆3,076May 22, 2026Updated 5 months ago
- Tactics for discharging Lean goals into SMT solvers.☆315Oct 20, 2026Updated last week
- A curated set of links to formal methods involving provable code.☆227Dec 12, 2021Updated 4 years ago
- A mechanisation of Wasm in Rocq☆127Oct 13, 2026Updated 2 weeks ago
- Serverless GPU API endpoints on Runpod - Get Bonus Credits • AdSkip the infrastructure headaches. Auto-scaling, pay-as-you-go, no-ops approach lets you focus on innovating your application.
- Datalog compiler embedded in Rust as a procedural macro☆535Dec 14, 2025Updated 10 months ago
- Propositional logic with types in Rust☆65Aug 1, 2023Updated 3 years ago
- Concurrency permutation testing tool for Rust.☆2,851Feb 20, 2026Updated 8 months ago
- property testing and verification front-end for Rust☆260Oct 3, 2026Updated 3 weeks ago
- Coq Protocol Playground with Se(xp)rialization of Internal Structures.☆136Nov 27, 2025Updated 11 months ago
- Metaprogramming, verified meta-theory and implementation of Rocq in Rocq☆562Oct 13, 2026Updated 2 weeks ago
- Verify naive = datafrog-opt, in rust/polonius☆17Jun 26, 2025Updated last year