Formal Verification
Showing 36 of 84 projects
A high-performance theorem prover and satisfiability modulo theories (SMT) solver from Microsoft Research.
An interactive theorem prover providing a formal language to write mathematical definitions, algorithms, and theorems with machine-checked proof development.
An interactive theorem prover providing a formal language to write mathematical definitions, algorithms, and theorems with machine-checked proof development.
A state machine based programming language for formally modeling and analyzing complex distributed systems.
A bit-precise model checker for verifying safety and correctness properties in Rust code.
A tool for statically verifying the correctness of Rust code using formal specifications and automated solvers.
A safe and flexible programming language for blockchain smart contracts with built-in resource safety.
An executable specification language with delightful tooling based on the Temporal Logic of Actions (TLA+)
A Coq library for formalizing Homotopy Type Theory, interpreting type theory into homotopy theory.
A domain-specific language for specifying, implementing, and verifying cryptographic algorithms with executable formal specifications.
A Coq library formalizing mathematics using univalent foundations and homotopy type theory.
A language for formally specifying instruction-set architecture (ISA) semantics with tooling for emulators, documentation, and verification.
A curated list of awesome resources for the Ada and SPARK programming languages, including compilers, libraries, tools, and applications.
Synthesizes formally verified, correct-by-construction C, Rust, Go, and other language code for cryptographic field arithmetic primitives.
An axiom-free formalization of category theory in Coq for representation, manipulation, and realization of categorical terms.
A collection of smart contracts that have undergone formal verification using the K-framework to ensure correctness against specifications.
A usable, easy, and safe pure-Rust cryptography library for AEAD, hashing, KDF, ECDH, and more.
An automated solver for proving the equivalence of SQL queries using formal verification.
An extensive and coherent library of formalized mathematical theories built on the Coq/Rocq proof assistant with SSReflect.
A Coq framework for implementing and formally verifying distributed systems with support for multiple fault models.
A formal semantics of the Ethereum Virtual Machine (EVM) written in the K framework, enabling verification and symbolic execution of smart contracts.
A symbolic model checker for TLA+ and Quint specifications, translating them into SMT constraints for verification.
A collection of hard-to-discover tips, tricks, and features for the Coq proof assistant.
A JavaScript port of the Coq proof assistant that runs entirely in the browser, enabling interactive theorem proving online.
A Neovim plugin providing comprehensive language support for the Lean theorem prover, including an infoview, abbreviations, and LSP integration.
A project formalizing the Rocq proof assistant in Rocq itself, providing tools for metaprogramming and developing certified plugins.
A research prototype tool for modular formal verification of C, Rust, and Java programs using separation logic.
A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
A lightweight proof assistant for teaching and exploring formal verification, accompanying The Little Prover book.
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources.
A language and compiler for writing high-assurance, high-speed cryptographic implementations.
An automatic formal verification tool that uses separation logic to verify memory safety of C programs.
A Vim plugin for interactive Rocq (Coq) proof development, providing IDE-like features within the editor.
A programming language and verification toolset for engineering high-reliability, safety-critical, and secure applications.
A randomized property-based testing plugin for Coq, enabling automated test generation and verification within proof assistants.
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.