Vale - Assembly language

Vale, aka Verified Assembly Language for Everest, is an assembly language created in 2017 by Chris Hawblitzel.

#876on PLDB

7Years Old

Download source code:

git clone https://github.com/project-everest/vale

Vale is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code. It uses existing verification frameworks, such as Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux. Additional architectures and platforms can be supported with no changes to the Vale tool.

Tags: assembly language
Vale is developed on GitHub and has 261 stars
Vale is written in reStructuredText, F#, XML, Python, Bourne shell, Markdown, C#, Dockerfile, C, Bash, PowerShell, JSON, OCaml, Make
See also: (1 related languages) F*

Example from the web:

procedure ReadA(ghost a:seq(uint32),inline b:bool)
 reads r0; mem;
 modifies r1;
 requires
  length(a) >= 3;
  a[0] <= 100;
  a[1] <= 100;
  forall i :: 0 <= i < length(a) ==>
   InMem(r0 + 4 * i, mem)
   && mem[r0 + 4 * i] == a[i];
 ensures
  b ==> r1 == a[0] + 1;
  !b ==> r1 == a[1] + 1;
{
 inline if (b) {
  LDR(r1, r0, 0); //load memory [r0+0] into r1
  AddOne(r1);
 } else {
  LDR(r1, r0, 4); //load memory [r0+4] into r1
  AddOne(r1);
 }
}
procedure{:recursive} AddNToR7(inline n:nat)
 modifies r7;
 requires r7 + n <= 0xffffffff;
 ensures r7 == old(r7) + n;
{
 inline if (n > 0) {
  AddOne(r7);
  AddNToR7(n - 1);
}

Language features

Feature	Supported	Example	Token
Comments	✓	// A comment
Line Comments	✓	// A comment	//
Semantic Indentation	X