formal

Proven at compile time

The compiler is not a checker you can argue with. It rejects the program unless it has a proof.

The same program, every language

formal usually compiles to fewer instructions because it ships no runtime, no libc, and no garbage collector beneath it.

print("Hello World!\n")
exit(0)

formal new hello_world && cd hello_world
cargo run
grep -cE '^    [a-z]' build/main.s

fn main() {
    println!("Hello World!");
}

cargo new hw && cd hw
echo 'fn main() { println!("Hello World!"); }' > src/main.rs
CARGO_PROFILE_RELEASE_OPT_LEVEL=z CARGO_PROFILE_RELEASE_LTO=true CARGO_PROFILE_RELEASE_CODEGEN_UNITS=1 CARGO_PROFILE_RELEASE_PANIC=abort CARGO_PROFILE_RELEASE_STRIP=true RUSTFLAGS='-Zlocation-detail=none -Zfmt-debug=none -Zunstable-options -Cpanic=immediate-abort' cargo +nightly build --release --target x86_64-unknown-linux-musl -Zbuild-std=std,panic_abort -Zbuild-std-features=
objdump -d target/x86_64-unknown-linux-musl/release/hw | grep -cE '^[[:space:]]+[0-9a-f]+:'

Every figure is measured by the project's own comparison test against pinned toolchains. Hover an execution time for the host and QEMU setup it was measured under.

One statement, one instruction

Two layers, kept deliberately close. Every simple statement lowers to exactly one RISC-V instruction or directive, and if, while and require each lower to a small fixed pattern of branches plus generated labels. No register allocation, no hidden control flow, the C-like cost model where the price of a line is visible at the call site, and inline assembly always one asm: block away.

value: global _              ->  #$ value global _         define; locality named, type inferred
welcome: _ [u8*13]           ->  #$ welcome _ [u8 ... u8]  _ locality = search thread, then global
nums: [u32]*4 = [2, 7, 0, 1] ->  #$ nums thread [u32 ...]  locality elided = thread; list initialiser
t0 = &value                  ->  la t0, value              address of a variable
t0 = type(welcome)           ->  #& t0, welcome            address of the runtime type descriptor
t0 = csr(mhartid)            ->  csrr t0, mhartid          which hart am I?
t1 = 0x10000000              ->  li t1, 0x10000000         load immediate
t1 = t1 + 1                  ->  addi t1, t1, 1            register +/- immediate
t0[0] = t1                   ->  #] t1, 0(t0)              store element 0 (sized by its type)
t1 = t0[2]                   ->  #[ t1, 2(t0)              load element 2 (sized by its type)
t0[0:4] = t1                 ->  sw t1, 0(t0)              raw byte slice: memory with no type
t1 = t0[8:16]                ->  ld t1, 8(t0)              raw load (1 = lb, 4 = lw, 8 = ld)
section 0x100 0x200 rw       ->  #@ 0x100 0x200 rw         declare an accessible region
fail                         ->  #!                        must be proven unreachable
unreachable                  ->  #?                        end of execution
asm:                         ->  (each indented line       inline assembly
    wfi                          emitted verbatim)

require t1 < t2              # fail unless t1 < t2  (one-line `if not cond: fail`)
if t0 == 0:                 # run the block when the condition holds
    t1 = t0[0]
while t5 != t2:             # top-tested loop
    t5 = t5 + 1

A runtime index is not supported yet, so arr[i] with i in a register is written out as t = i * 4 for a 4-byte element, then p = base + t, then p[0], which keeps the cost of the address arithmetic visible and is why the fannkuch sample hand-desugars its inner loop.

# you write
value: global _
welcome: _ [u8*13]

# the compiler emits
.section .data
__welcome_type:
    .dword 8                # List
    .dword __welcome_subtypes
    .dword 13               # length

.section .bss
    .balign 8
value:
    .zero 4
    .balign 8
welcome:
    .zero 13

# you write: a 25-byte record stride
t0 = t0 + 25

# the compiler emits: 8, the bytes the
# program can actually reach
    addi t0, t0, 8

End to end: source to booted RISC-V

The project's real end-to-end test, tests/uart_hello/. The source races two harts on an inferred global, has hart 0 check the message's runtime type descriptor (the program inspects its own inferred types), then prints over the UART.

# Do racy arithmetic with an undefined variable.
# Use global locality so the load/stores are racy.
value: global _
t0 = &value

# Set to 0
t1 = 0
t0[0:4] = t1

# Do non-atomic addition
t1 = t0[0:4]
t1 = t1 + 1
t0[0:4] = t1

# The proof obligation: value < 4 on every interleaving (`require` lowers to
# a branch over `#!`, the `fail` marker).
t1 = t0[0:4]
t2 = 4
require t1 < t2

# Use hart 0 to output a message; every other hart skips straight to the
# `wfi` at the end.
t0 = csr(mhartid)
if t0 == 0:
    welcome: _ [u8*13]
    # H  e  l  l  o     W  o  r  l  d  !  0
    # Type exploration doesn't explore list types since they are infinite, so
    # to define a list a user must define it manually.
    # In this case we leave the locality as unspecified which will default to `thread`.

    # Declare string
    # Get address of type structure
    t0 = type(welcome)

    # Check variable is list
    t2 = 8  # Load list type number
    t1 = t0[0]  # Load type type number
    require t1 == t2

    # Check list length
    t0 = t0 + 16  # Increment address to point at length
    t1 = t0[0]  # Load length
    t2 = 13  # Load desired length
    require t1 == t2

    # Check all values in list are u8
    t0 = t0 - 8  # Decrement address to point at list address
    t0 = t0[0]  # Load list address

    t5 = 0  # Use t5 as the counter
    while t5 != t2:
        t3 = t0[0:8]  # Load type of list item
        t4 = 0  # Load byte type number
        require t3 == t4
        t0 = t0 + 25  # Increment list item address (8+8+8+1)
        t5 = t5 + 1  # Increment the count

    # Set string
    t0 = &welcome
    t1 = 72  # H
    t0[0] = t1
    t1 = 101  # e
    t0[1] = t1
    t1 = 108  # l
    t0[2] = t1
    t1 = 108  # l
    t0[3] = t1
    t1 = 111  # o
    t0[4] = t1
    t1 = 32  # space
    t0[5] = t1
    t1 = 87  # W
    t0[6] = t1
    t1 = 111  # o
    t0[7] = t1
    t1 = 114  # r
    t0[8] = t1
    t1 = 108  # l
    t0[9] = t1
    t1 = 100  # d
    t0[10] = t1
    t1 = 33  # !
    t0[11] = t1
    t1 = 0  # NUL terminator
    t0[12] = t1

    # Output message
    a0 = &welcome  # Load message address
    t1 = 0x10000000  # Load character device address
    t2 = a0[0]  # Load the first character
    while t2 != 0:
        t1[0:1] = t2  # Store character into character device
        a0 = a0 + 1  # Add 1 message address
        t2 = a0[0]  # Load next character

asm:
    wfi
unreachable

.global _start
_start:
    #$ value global _
    la t0, value
    li t1, 0
    sw t1, 0(t0)
    lw t1, 0(t0)
    addi t1, t1, 1
    sw t1, 0(t0)
    lw t1, 0(t0)
    li t2, 4
    blt t1, t2, _l0
_l0:
    csrr t0, mhartid
    bnez t0, _l1
    #$ welcome _ [u8 u8 u8 u8 u8 u8 u8 u8 u8 u8 u8 u8 u8]
    la t0, __welcome_type  # #& t0, welcome
    li t2, 8
    ld t1, 0(t0)  # #[ t1, 0(t0)
    beq t1, t2, _l2
_l2:
    addi t0, t0, 16
    ld t1, 0(t0)  # #[ t1, 0(t0)
    li t2, 13
    beq t1, t2, _l3
_l3:
    addi t0, t0, -8
    ld t0, 0(t0)  # #[ t0, 0(t0)
    li t5, 0
_l4:
    beq t5, t2, _l5
    ld t3, 0(t0)
    li t4, 0
    beq t3, t4, _l6
_l6:
    addi t0, t0, 8
    addi t5, t5, 1
    j _l4
_l5:
    la t0, welcome
    li t1, 72
    sb t1, 0(t0)  # #] t1, 0(t0)
    li t1, 101
    sb t1, 1(t0)  # #] t1, 1(t0)
    li t1, 108
    sb t1, 2(t0)  # #] t1, 2(t0)
    li t1, 108
    sb t1, 3(t0)  # #] t1, 3(t0)
    li t1, 111
    sb t1, 4(t0)  # #] t1, 4(t0)
    li t1, 32
    sb t1, 5(t0)  # #] t1, 5(t0)
    li t1, 87
    sb t1, 6(t0)  # #] t1, 6(t0)
    li t1, 111
    sb t1, 7(t0)  # #] t1, 7(t0)
    li t1, 114
    sb t1, 8(t0)  # #] t1, 8(t0)
    li t1, 108
    sb t1, 9(t0)  # #] t1, 9(t0)
    li t1, 100
    sb t1, 10(t0)  # #] t1, 10(t0)
    li t1, 33
    sb t1, 11(t0)  # #] t1, 11(t0)
    li t1, 0
    sb t1, 12(t0)  # #] t1, 12(t0)
    la a0, welcome
    li t1, 0x10000000
    lbu t2, 0(a0)  # #[ t2, 0(a0)
_l7:
    beqz t2, _l8
    sb t2, 0(t1)
    addi a0, a0, 1
    lbu t2, 0(a0)  # #[ t2, 0(a0)
    j _l7
_l8:
_l1:
    wfi
    j __halt  # unreachable (program end)
__halt:
    wfi
    j __halt

.section .data
__welcome_type:
    .dword 8                # List
    .dword __welcome_subtypes      # subtypes
    .dword 13                # length
__welcome_subtypes:
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0
    .dword 0

.section .bss
    .balign 8
value:
    .zero 4
    .balign 8
welcome:
    .zero 13

translate (one statement, one instruction or directive) → parse → verify (2,111,465 machine states across 1- and 2-hart systems) → infer value: u32, welcome: thread [u8 × 13] → remove dead code & never-taken branches → compact the layout → emit

$ cargo nt uart_hello
PASS [25.001s] formal::uart_hello uart_hello

The dialect underneath

Under the surface language sits the verification target: RISC-V assembly plus seven directives. Every directive starts with #, the RISC-V comment character, so any formal program is also a plain assembly file.