awslabs/aws-lc-verification
View on GitHub ↗ ★ 73 Rocq Prover
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.
3 mentions on Hacker News by 3 people: 0 stories, 3 comments · first 2024-09-14 · latest 2024-12-20
20082026
-
…the use of structured programming. It's equally applicable to concurrent programming though. [1]: https://github.com/awslabs/aws-lc-verification [2]: https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.p...
comment by spinningslate · 2024-12-20 · in How concurrency works: A visual guide -
…are formally generated or formally verified (see https://github.com/awslabs/s2n-bignum and https://github.com/awslabs/aws-lc-verification for directly related work) and also make massive improvements to the constant-timeness of the…
comment by colmmacc · 2024-10-22 · in Rustls Outperforms OpenSSL and BoringSSL -
…(or FS) authoring space but AWS uses formal verification for their ... fork? ... of BoringSSL et al https://github.com/awslabs/aws-lc-verification#aws-libcrypto...
comment by mdaniel · 2024-09-14 · in My 71 TiB ZFS NAS After 10 Years and Zero Drive Failures