A verification toolchain for Rust programs
-
Updated
Jul 19, 2024 - OCaml
A verification toolchain for Rust programs
A cryptographic framework, proven for correctness in SPARK
Scalable symbolic-numeric set computations in Julia
CakeML: A Verified Implementation of ML
Toolset to capture, simulate, synthesize and verify graph models
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
ACL2 System and Books as Maintained by the Community
The P programming language.
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
The formally verified crypto library for Rust
Creusot helps you prove your code is correct in an automated fashion.
HACL*, a formally verified cryptographic library written in F*
The specification testing tool for the Move language based on the mutant generation.
KeY Theorem Prover for Deductive Java Verification
BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)
Interface with the rustc compiler for the purpose of program verification
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs!
Assignments for module: CA648
alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, and 2023)
Add a description, image, and links to the formal-verification topic page so that developers can more easily learn about it.
To associate your repository with the formal-verification topic, visit your repo's landing page and select "manage topics."