Vale

code edit

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

Source code:

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

#918on PLDB

7Years Old

Verified Assembly Language for Everest

Vale is developed on GitHub and has 217 stars

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);
}

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

Language features