the champagne of beta embedded databases
Creusot helps you prove your code is correct in an automated fashion.
CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
Interface with the rustc compiler for the purpose of program verification
Library for building symbolically executable stack-based virtual machines
A toy formally-specified Computer Algebra library written in Rust and formalized in Lean 4
symbolic EVM execution engine written in Rust
Online engine for reasoning about the Noise Protocol Framework.
Let's build a symbolic model checker from scratch in Rust !
The Supervisionary proof-checking kernel for higher-order logic
Big-step, small-step and axiomatic semantics for the IMP language (unofficial)
WASM tools with non deterministic operations support
Thunder is a model checker implemented in Rust, created during the first iteration of the practical course on model checking at RWTH Aachen.
Implementation of SHA3 in Rust, verified in Lean with Aeneas.
Let's try to implement some model checking algorithms in Rust, just for fun!
Independent implementation of the pattern matching algorithms in Maude.
A deductive program verification tool for MicroViper programming language
Add a description, image, and links to the formal-methods topic page so that developers can more easily learn about it.
To associate your repository with the formal-methods topic, visit your repo's landing page and select "manage topics."