Formal Verification
Showing 36 of 178 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 extensive and coherent library of formalized mathematical theories built on the Coq/Rocq proof assistant with SSReflect.
An automated solver for proving the equivalence of SQL queries using formal verification.
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 Neovim plugin providing comprehensive language support for the Lean theorem prover, including an infoview, abbreviations, and LSP integration.
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 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.
Related Tags
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.