Alternatives and similar repositories for awesome-formal-verification

Users that are interested in awesome-formal-verification are comparing it to the libraries listed below

• model-checking / rust-lean-models
  Lean models of Rust libraries
  ☆21Updated last year
• opencompl / lean-mlir
  A minimal development of SSA theory
  ☆184Updated this week
• awslabs / aws-lc-verification
  This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal…
  ☆59Updated 2 weeks ago
• viperproject / silver
  Definition of the Viper intermediate verification language.
  ☆89Updated this week
• bitwuzla / bitwuzla
  Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays a…
  ☆282Updated last week
• uclid-org / uclid
  UCLID5: formal modeling, verification, and synthesis of computational systems
  ☆149Updated 3 months ago
• kenmcmil / ivy
  IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform f…
  ☆96Updated 3 weeks ago
• lfi-project / lfi
  Top-level repository for LFI: Practical, Efficient, and Secure Software-based Sandboxing
  ☆90Updated 2 months ago
• kind2-mc / kind2
  Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
  ☆105Updated this week
• philzook58 / awesome-egraphs
  An awesome list of e-graph resources
  ☆243Updated this week
• rems-project / isla
  Symbolic execution tool for Sail ISA specifications
  ☆78Updated last month
• seL4 / microkit
  Microkit - A simple operating system framework for the seL4 microkernel
  ☆138Updated last week
• rems-project / rmem
  rmem public repo
  ☆48Updated 4 months ago
• mit-plv / bedrock2
  A work-in-progress language and compiler for verified low-level programming
  ☆313Updated this week
• CTSRD-CHERI / llvm-project
  Fork of LLVM adding CHERI support
  ☆57Updated this week
• model-checking / cbmc-viewer
  CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
  ☆31Updated last week
• Boolector / boolector
  A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
  ☆352Updated last year
• jasmin-lang / jasmin
  Language for high-assurance and high-speed cryptography
  ☆311Updated this week
• project-oak / silveroak
  Formal specification and verification of hardware, especially for security and privacy.
  ☆126Updated 3 years ago
• viperproject / silicon
  Symbolic-execution-based verifier for the Viper intermediate verification language.
  ☆115Updated this week
• vellvm / vellvm
  The Vellvm (Verified LLVM) coq development.
  ☆443Updated last week
• uw-unsat / exoverifier
  ☆17Updated 2 years ago
• leanprover / LNSym
  Armv8 Native Code Symbolic Simulator in Lean
  ☆86Updated 2 months ago
• au-ts / lionsos
  A secure, fast, and adaptable OS based on the seL4 microkernel
  ☆146Updated last week
• uwplse / ruler
  Rewrite Rule Inference Using Equality Saturation
  ☆140Updated 4 months ago
• Sophietje / Verification-Tool-Overview
  Information about verification tools. Browse the data at https://slebok.github.io/proverb/
  ☆30Updated last year
• CTSRD-CHERI / cheribuild
  Easily build and run CHERI related projects
  ☆82Updated this week
• clarksmr / sf-lectures
  Software Foundations
  ☆143Updated last year
• mit-plv / riscv-coq
  RISC-V Specification in Coq
  ☆116Updated this week
• PrincetonUniversity / VST
  Verified Software Toolchain
  ☆470Updated this week