Formal Methods
Showing 19 of 19 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.
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.