verus-lang / verus-analyzer
A Verus compiler front-end for IDEs (derived from rust-analyzer)
☆15Updated this week
Alternatives and similar repositories for verus-analyzer:
Users that are interested in verus-analyzer are comparing it to the libraries listed below
- Interface with the rustc compiler for the purpose of program verification☆115Updated this week
- A verification toolchain for Rust programs☆237Updated this week
- A language for symbolic transitions system, inspired by Ivy.☆69Updated 10 months ago
- Rewrite Rule Inference Using Equality Saturation☆121Updated 8 months ago
- Lean 4 port of Iris, a higher-order concurrent separation logic framework☆78Updated 3 weeks ago
- RustHorn: A CHC-based automated verifier for Rust☆74Updated 2 weeks ago
- Definition of the Viper intermediate verification language.☆81Updated last week
- Lean models of Rust libraries☆12Updated 5 months ago
- Visual Studio Code Extension and Language Server Protocol for Coq☆159Updated last week
- SMTscope automatically analyses and visualises SMT solver execution traces.☆24Updated this week
- ☆39Updated 2 months ago
- Armv8 Native Code Symbolic Simulator in Lean☆72Updated 2 months ago
- Experiments in automation for Lean☆92Updated last week
- A Seamless, Interactive Tactic Learner and Prover for Coq☆59Updated 2 weeks ago
- An automated deductive program verifier based on concurrent separation logic☆14Updated this week
- A (WIP) equality saturation tactic for Lean based on egg.☆55Updated last week
- This package provides an interface and foundation for verified SAT reasoning☆51Updated 5 months ago
- Alternative Mizar proof checker (http://mizar.org/) written in Rust☆50Updated 6 months ago
- An awesome list of e-graph resources☆126Updated last month
- Compositional Verification of Composite Byzantine Protocols☆12Updated 5 months ago
- An attempt at safe imperative GPU programming.☆29Updated 2 months ago
- Symbolic-execution-based verifier for the Viper intermediate verification language.☆93Updated this week
- Tactics for discharging Lean goals into SMT solvers.☆164Updated 3 weeks ago
- Separation Logic Proofs in Lean☆34Updated 2 months ago
- Rust bindings for the Lean 4 proof assistant☆21Updated this week
- A modern (trail saving, clause subsumption/vivification, learning-rate based selecting, rephrase) CDCL SAT solver in Rust☆87Updated last week
- VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification …☆43Updated last month
- embedding MLIR in LEAN☆47Updated 8 months ago
- Cerberus C semantics☆61Updated this week
- Coq code formatter☆22Updated this week