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.
☆56Updated last month
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:
- A foundational framework for modular cryptographic proofs in Coq☆66Updated 2 weeks ago
- ☆177Updated this week
- Language for high-assurance and high-speed cryptography☆306Updated this week
- Specifications of cryptographic algorithms in Cryptol☆41Updated 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…☆95Updated 3 weeks ago
- Armv8 Native Code Symbolic Simulator in Lean☆84Updated last week
- CN separation logic refinement type system for C☆28Updated last week
- Cerberus C semantics☆66Updated this week
- Crypto library☆62Updated last month
- Foundational Cryptography Framework for machine-checked proofs of cryptography.☆52Updated 2 months ago
- RISC-V Specification in Coq☆116Updated last month
- VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification …☆46Updated 7 months ago
- Compositional Verification of Security Protocols☆19Updated 2 weeks ago
- DaisyNFS is an NFS server verified using Dafny and Perennial.☆38Updated 10 months ago
- Automated generation of provably secure, zero-copy parsers from format specifications☆285Updated this week
- The VerCors verification toolset for verifying parallel and concurrent software☆78Updated this week
- The CBMC starter kit makes it easy to add CBMC verification to a software project.☆46Updated 2 weeks ago
- Libraries useful for Dafny programs☆45Updated this week
- Definition of the Viper intermediate verification language.☆88Updated last week
- Symbolic-execution-based verifier for the Viper intermediate verification language.☆112Updated last week
- Assembly super-optimization via constraint solving☆216Updated this week
- SRI Sally: A model checker for infinite-state systems.☆73Updated 3 weeks ago
- A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development sna…☆131Updated last month
- Multi-engine SMT-based automatic model checker for safety properties of Lustre programs☆105Updated this week
- Verification-condition-generation-based verifier for the Viper intermediate verification language.☆31Updated 3 weeks ago
- Communication between Coq and SAT/SMT solvers☆160Updated 11 months ago
- Public snapshots of "ACSL by Example"☆113Updated 3 months ago
- CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives☆62Updated last year
- Goose converts a subset of Go to Rocq☆126Updated last week
- System for verifying the correctness of generated Copilot programs☆17Updated 3 months ago