Hacl-star Alternatives

hacl-star reviews and mentions

• HACL: A High-Assurance Cryptographic Library
  1 project | news.ycombinator.com | 9 Jun 2024
• F* – A Proof-Oriented Programming Language
  4 projects | news.ycombinator.com | 16 May 2024

  F* existed before Project Everest, but Everest did power a lot of its development.

  We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/

  Some of it is deployed in production systems:

  * Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-hard...

  * Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star

• One step forward, an easier interoperability between Rust and Haskell | IOG Engineering
  1 project | /r/haskell | 27 Jan 2023

  Nice work. About cryptonite: have IOG considered using crypto primitives provided by HACL*/evercrypt?

• Let's collect relatively new research programming languages in this thread
  19 projects | /r/ProgrammingLanguages | 15 Nov 2022

  Jasmin and F* don't have similar goals, Jasmin is a language designed to precisely express low-level code, while F* is a generalist language for verified programming. There is a subsystem of F* that performs extraction to "readable C code", Karamel (used to be called Kremlin), but you get the usual limitations of C code as a high-level assembler, and also an embedded assembly layer built on Vale. Project Everest therefore generates artifacts that are a mix of C and assembly, rather than a new low-level language design as Jasmin.

• Ten Years of TypeScript
  8 projects | news.ycombinator.com | 1 Oct 2022
• Securing your crypto wallet in a way that gives respect to what cryptography actually is
  3 projects | /r/CryptoCurrency | 21 Nov 2021

  With that said, it's a very good thought to make sure that the software you're using is actually secure before trusting it. Personally, I think it's safe to use GnuPG and KeePass/Bitwarden, which have all been audited by the likes of Cure53, but if you're really paranoid, you could always use a formally-verified implementation of your desired algorithm (many are supplied in HACL*, for example)... In this case, I use the term "formally-verified" to mean that the implementation is mathematically proven to guarantee the properties of the algorithm (i.e., there are no "bugs" that affect output at the implementation level)...

• 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

  This is SO exciting!!! Ituses https://github.com/project-everest/hacl-star - a formally verified cryptography library. And it compiles down to C code, so I suppose it's fast.

• Formal is fast: performance analysis and tuning of SPARKNaCl
  2 projects | /r/ada | 11 Feb 2021

  Whats cool with that project and overlaps with SPARKNaCI would be the HACL* Library. Its purpose is to provide a formally verified library of modern cryptographic algorithms all written in a subset of F* called Low* and compiled to C using a compiler called KreMLin. The outputs of this are already being used Firefox, see here & here.

• A Memory Safe TLS Module for the Apache HTTP Server
  1 project | /r/rust | 2 Feb 2021

  Reminds me a little of the Everest project. Sadly, I'm not seeing much recent Everest activity on their web page or github.

• A note from our sponsor - InfluxDB
  www.influxdata.com | 15 Jul 2025

  InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now. Learn more →