Formal Methods
Showing 27 of 27 projects
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 static analyzer for C/C++ that detects runtime errors using abstract interpretation theory.
A personal wiki containing notes and drafts about software quality assurance topics and practices.
A curated wiki and collection of notes about software quality assurance, testing, and best practices.
An executable specification language with delightful tooling based on the Temporal Logic of Actions (TLA+)
A curated list of resources for theoretical computer science, emphasizing mathematical techniques and rigor.
A curated list of resources for learning theoretical computer science, emphasizing mathematical techniques and rigor.
An axiom-free formalization of category theory in Coq for representation, manipulation, and realization of categorical terms.
An extensive and coherent library of formalized mathematical theories built on the Coq/Rocq proof assistant with SSReflect.
A command-line tool for generating runtime monitors for flight and robotics applications from formal specifications.
A JavaScript port of the Coq proof assistant that runs entirely in the browser, enabling interactive theorem proving online.
A tool for writing definitions of programming languages and calculi, generating LaTeX and formal proof assistant code from a concise ASCII notation.
A C++ library implementing the Responsibility Sensitive Safety (RSS) model for autonomous vehicle decision-making.
A library of Coq definitions, theorems, and tactics for use in other Coq developments.
A toolset for formal specification and generation of verifiable binary parsers, message generators, and protocol state machines.
A Coq library for mechanizing programming language metatheory with locally nameless representation of binders.
A collection of statements and proofs for 100 famous mathematical theorems formalized in the Coq proof assistant.
Coq formalization of program logics (Hoare logic, separation logic, concurrent separation logic) for verifying imperative and concurrent programs.
Mutation analysis tool for Coq verification projects to detect incomplete specifications.
A unified Coq library for bit vectors used across multiple MIT research projects.
A Java static analysis tool that translates Java code into LiSA's IR and runs configurable abstract interpretation analyses for bug detection and verification.
A Coq library providing enhanced coinductive proof methods based on the 'companion' concept from coinduction theory.
A formally verified XML library in SPARK 2014, proven free of runtime errors and with bounded stack usage for secure untrusted data processing.
A SPARK library for building portable, verifiable, and high-performance trusted components in component-based systems.
A model-based end-to-end testing framework for Cosmos SDK blockchains, using TLA+ models to generate and execute test scenarios.
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.