project-everest/vale

View on GitHub ↗ ★ 321 F#

Verified Assembly Language for Everest

7 mentions on Hacker News by 7 people: 0 stories, 7 comments · first 2017-07-17 · latest 2026-05-20

Mentions per year 7 mentions · busiest year 2017 (2)

20082026

All Stories Comments Newest Top Oldest

…defined Hoare logic that can talk about total correctness, not just [1]'s partial correctness. [0] https://github.com/project-everest/vale [1] https://nickbenton.name/coqasm.pdf
comment by addaon · 2026-05-20 · in Everything in C is undefined behavior
…https://en.m.wikipedia.org/wiki/Typed_assembly_language Which eventually grew to stuff like this, https://github.com/project-everest/vale
comment by pjmlp · 2024-10-03 · in A C++ Developer Learns Assembly
…new unambiguous name asap in order get more visibility. Otherwise, it looks very promising! [1] https://github.com/project-everest/vale [2] https://en.m.wikipedia.org/wiki/Vala_(programming_language)
comment by Squonk42 · 2022-06-18 · in The Vale Programming Language
…http://www.fftw.org/ http://flopoco.gforge.inria.fr/ https://github.com/FStarLang/kremlin https://github.com/project-everest/vale
comment by lapinot · 2021-03-21 · in The Generic Dilemma (2009)
…Vale[0], but at that point, just use miTLS[1] to have a completely verified TLS implementation. [0] https://github.com/project-everest/vale [1] https://mitls.org/
comment by PyroLagus · 2019-07-19 · in A Rust-based TLS library outperformed OpenSSL in almost every category
…might enjoy: http://www.cs.cornell.edu/talc/ https://project-everest.github.io/assets/vale2017.pdf https://github.com/project-everest/vale
comment by nickpsecurity · 2017-10-09 · in X86 Proved: Coq Library for Modelling, Specification, Generation and Proof for X86
…we want it to have. [1] https://www.fstar-lang.org/ [2] https://github.com/mitls/hacl-star [3] https://github.com/project-everest/vale
comment by zx2c4 · 2017-07-17 · in Formal verification of the WireGuard protocol