praborrow-prover
| Crates.io | praborrow-prover |
| lib.rs | praborrow-prover |
| version | 1.2.2 |
| created_at | 2026-01-09 16:54:23.036753+00 |
| updated_at | 2026-01-14 03:30:29.176365+00 |
| description | SMT-based formal verification for PraBorrow. Interfaces with Z3 theorem prover to mathematically validate Constitution invariants. |
| homepage | |
| repository | https://github.com/ireddragonicy/PraBorrow |
| max_upload_size | |
| id | 2032392 |
| size | 112,993 |
Ndik (IRedDragonICY)
documentation
README
praborrow-prover
English | Indonesia
Formal verification engine for the PraBorrow framework.
Overview
This crate provides the constraint solving and proof generation capabilities for PraBorrow. It integrates with Z3 to verify invariants specified in praborrow-defense at both compile-time and runtime.
Key Features
-
Z3 Integration: Bindings to the Z3 theorem prover for SMT solving.
-
Invariant Parsing: Parsing logic for logical assertions defined in contracts.
-
Validity Checking: Automated verification of boolean expressions against sovereign state.