awslabs / aws-lc-verificationLinks
This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.
☆60Updated last week
Alternatives and similar repositories for aws-lc-verification
Users that are interested in aws-lc-verification are comparing it to the libraries listed below
Sorting:
- Language for high-assurance and high-speed cryptography☆313Updated last week
- ☆186Updated last week
- IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform f…☆99Updated last month
- A foundational framework for modular cryptographic proofs in Coq☆69Updated 2 weeks ago
- Armv8 Native Code Symbolic Simulator in Lean☆87Updated 2 months ago
- Specifications of cryptographic algorithms in Cryptol☆43Updated 2 weeks ago
- CN separation logic refinement type system for C☆38Updated this week
- Cerberus C semantics☆71Updated 2 months ago
- The VerCors verification toolset for verifying parallel and concurrent software☆80Updated this week
- Definition of the Viper intermediate verification language.☆90Updated 2 weeks ago
- CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives☆61Updated last year
- Automated generation of provably secure, zero-copy parsers from format specifications☆289Updated 2 weeks ago
- Compositional Verification of Security Protocols☆22Updated 2 weeks ago
- Crypto library☆65Updated 2 weeks ago
- SRI Sally: A model checker for infinite-state systems.☆75Updated 2 months ago
- VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification …☆45Updated 9 months ago
- ☆41Updated 3 months ago
- System for verifying the correctness of generated Copilot programs☆17Updated 5 months ago
- RISC-V Specification in Coq☆116Updated 2 weeks ago
- The Squirrel Prover repository. An interactive prover for the formal verification of security protocols.☆54Updated 2 weeks ago
- Files and tools for SMT-COMP, the International Satisfiability Modulo Theories Competition.☆30Updated 8 months ago
- ☆53Updated last week
- A language for symbolic transitions system, inspired by Ivy.☆70Updated last month
- A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development sna…☆148Updated 2 weeks ago
- Symbolic-execution-based verifier for the Viper intermediate verification language.☆117Updated this week
- ☆17Updated last week
- Multi-engine SMT-based automatic model checker for safety properties of Lustre programs☆107Updated last week
- TriCera: a model checker for C programs☆25Updated last week
- Foundational Cryptography Framework for machine-checked proofs of cryptography.☆52Updated 3 weeks ago
- The CBMC starter kit makes it easy to add CBMC verification to a software project.☆47Updated 3 weeks ago