Evercrypt-rust Alternatives

Similar projects and alternatives to evercrypt-rust

FStar

42 2,567 9.9 F* evercrypt-rust VS FStar

A Proof-oriented Programming Language
dafny

31 2,665 9.7 C# evercrypt-rust VS dafny

Dafny is a verification-aware programming language
InfluxDB

www.influxdata.com sponsored

Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
RCIG_Coordination_Repo

18 240 3.5 HTML evercrypt-rust VS RCIG_Coordination_Repo

A Coordination repo for all things Rust Cryptography oriented
hacl-star

8 1,583 9.7 F* evercrypt-rust VS hacl-star

HACL*, a formally verified cryptographic library written in F*

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better evercrypt-rust alternative or higher similarity.

Suggest an alternative to evercrypt-rust

evercrypt-rust reviews and mentions

Posts with mentions or reviews of evercrypt-rust. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-09-13.

How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors
4 projects | news.ycombinator.com | 13 Sep 2021

CompCert is also very impressive. It's not, however, free software / open source (the source is available though)
https://www.absint.com/compcert/structure.htm
A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify.
F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack.
https://www.fstar-lang.org/
https://github.com/project-everest/hacl-star
https://www.mitls.org/
https://project-everest.github.io/
F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding
https://github.com/franziskuskiefer/evercrypt-rust
Also this F* stuff is all free software / open source, so it might become a very prevalent crypto and TLS stack
Awesome Rust Cryptography list compiled by the Rust Cryptography Interest Group (RCIG)
4 projects | /r/rust | 27 Jul 2021

evercrypt-rust (verified) Rust bindings for evercrypt, a set of high-performance HACL*-verified implementations of cryptographic primitives. bindings crate, bringing HACL-verified cryptographic primitives.