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.
☆61Updated 2 weeks ago
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☆327Updated this week
- IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform f…☆102Updated last week
- A foundational framework for modular cryptographic proofs in Coq☆73Updated last week
- ☆201Updated this week
- CN separation logic refinement type system for C☆44Updated last month
- Specifications of cryptographic algorithms in Cryptol☆46Updated last month
- Armv8 Native Code Symbolic Simulator in Lean☆96Updated 2 months ago
- Crypto library☆67Updated last month
- Foundational Cryptography Framework for machine-checked proofs of cryptography.☆55Updated 3 months ago
- RISC-V Specification in Coq☆116Updated 3 weeks ago
- CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives☆65Updated last year
- Definition of the Viper intermediate verification language.☆92Updated last week
- Compositional Verification of Security Protocols☆30Updated 3 weeks ago
- Libraries useful for Dafny programs☆47Updated 5 months ago
- Automated generation of provably secure, zero-copy parsers from format specifications☆303Updated this week
- Cerberus C semantics☆80Updated 2 weeks ago
- An Opinionated Formatter for Verus☆15Updated 2 weeks ago
- The Squirrel Prover repository. An interactive prover for the formal verification of security protocols.☆58Updated 3 months ago
- ☆34Updated 3 months ago
- A language for symbolic transitions system, inspired by Ivy.☆71Updated 4 months ago
- The VerCors verification toolset for verifying parallel and concurrent software☆85Updated this week
- A verifier for automated and interactive proofs about transition systems.☆179Updated 2 weeks ago
- SRI Sally: A model checker for infinite-state systems.☆75Updated 6 months ago
- Symbolic-execution-based verifier for the Viper intermediate verification language.☆126Updated last week
- Compositional Verification of Composite Byzantine Protocols☆13Updated last year
- DaisyNFS is an NFS server verified using Dafny and Perennial.☆43Updated last year
- ☆54Updated this week
- LLVM support for the lean theorem prover☆53Updated 4 years ago
- VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification …☆47Updated last year
- DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code☆18Updated last year