hacspec
silveroak
| hacspec | silveroak | |
|---|---|---|
| 3 | 3 | |
| 235 | 97 | |
| - | - | |
| 5.1 | 7.3 | |
| 3 months ago | almost 2 years ago | |
| Coq | Coq | |
| MIT License | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
hacspec
-
Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec
I have no idea what the legal weight is for a toml field so this repo really would benefit from having a formal copy of the Apache-2 license file https://github.com/hacspec/hax/blob/2da100068e9ae5e69e5b35bb... similar to its MIT friend https://github.com/hacspec/hacspec/blob/4ecc847fc944fe996e19...
-
Lets goo memory safe asm
†The "Rust" code would most likely need to be written in a strict subset of the language like Hacspec
-
Rustlang Cryptography Interest Group & Formal Verification Sync-up Call 2
Bas Spitter will be speaking on Hacspec and ConCert
silveroak
-
Type Theory Forall Podcast #13 - C/C++, Emacs, Haskell, and Coq. The Journey (John Wiegley)
Some other examples, Google has some people using Coq for hardware synthesis silveroak, there is a paper on using Coq for verifying some data structure at Facebook/Meta this year at CPP.
-
There's an ongoing effort to rewrite Principia Mathematica using Coq
There are ongoing research projects about that, you may want to have a look at Kôika (https://github.com/mit-plv/koika), Kami (https://github.com/mit-plv/kami), Lutsig (https://github.com/CakeML/hardware) and silveroak (https://github.com/project-oak/silveroak). Closer to HLS there is also Vericert (https://github.com/ymherklotz/vericert). There may be other research project I am unaware of, feel free to add them in a reply, I am interested in it.
- Silveroak - Formal specification and verification of hardware
What are some alternatives?
creusot - Creusot helps you prove your code is correct in an automated fashion. [Moved to: https://github.com/creusot-rs/creusot]
koika - A core language for rule-based hardware design 🦑
ConCert - A framework for smart contract verification in Coq
vericert - A formally verified high-level synthesis tool based on CompCert and written in Coq.
rust-crypto - A (mostly) pure-Rust implementation of various cryptographic algorithms.
practical-fm - A gently curated list of companies using verification formal methods in industry
proofs - My personal repository of formally verified mathematics.
kami - A Platform for High-Level Parametric Hardware Specification and its Modular Verification
zips - Zcash Improvement Proposals
saw-script - The SAW scripting language.
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
crucible - Crucible is a library for symbolic simulation of imperative programs