Sond: a language that proves your code

Six real CVEs, ported to Sond

A language that proves things is only interesting if it proves the things that actually hurt. So: six documented vulnerabilities from OpenSSL, FreeBSD, nginx, sudo, WavPack and dnsmasq, ported faithfully, bug and all. Then compiled.

CVE	Project	Bug class	Result
`CVE-2014-0160` Heartbleed	OpenSSL	Out-of-bounds read	Rejected at compile time
`CVE-2014-8612`	FreeBSD SCTP	Unvalidated attacker index	Rejected at compile time
`CVE-2019-1010315`	WavPack	Divide by zero	Rejected, with counterexample
`CVE-2026-4891`	dnsmasq DNSSEC	Negative length underflow	Rejected at compile time
`CVE-2017-7529`	nginx	Integer overflow defeats a bounds check	Compiles. Not caught.
`CVE-2021-3156` Baron Samedit	sudo	Off-by-one in a copy loop	Compiles. Not caught.

Four of six are compile errors. In every one of the six, the upstream fix compiles cleanly, which is the control that matters: a checker that rejects everything would prove nothing at all.

And the two misses share one cause. Both ports manipulate memory through raw address builtins rather than array indexing, and Sond's bounds checking applies to indexing only. Code that does its own pointer arithmetic is, today, outside the verifier entirely. That is not a footnote to bury: it is the honest limit of the current claim, it accounts for 100% of the failures in this corpus, and it is why a real pointer type is the next thing the language needs.

What is already built in Sond

A proof obligation you cannot discharge in practice is just a language nobody ships. So the question is not whether the idea is elegant, it's how far it reaches. Here is how far, today.

A kernel that boots on bare hardware

A kernel laid out like Linux 6.18 (arch/x86, kernel/printk, mm/page_alloc, drivers/tty/serial), written in Sond and compiled straight to a UEFI application. No OS underneath, no libc, no assembler stubs holding it up.

GDT · IDT · PIC remap · PIT at 100 Hz · 8250 UART · printk · bitmap page allocator. The transcript on the right is this kernel booting under QEMU/OVMF, through ExitBootServices and into its idle loop.

QEMU/OVMF · COM1 live boot

Sond Linux 6.18-sond booting...
[    0.000000] Exiting boot services...
[    0.000000] Boot services exited.
[    0.000000] Sond/Linux 6.18-sond
[    0.000000] CPU: 1 core, 64-bit mode
[    0.000000] Initializing GDT...   GDT loaded.
[    0.000000] Initializing IDT...   IDT loaded.
[    0.000000] Remapping PIC...      PIC remapped.
[    0.000000] Initializing PIT (100 Hz)...
[    0.000000] Interrupts enabled.
[    0.000000] Sond/Linux 6.18-sond booted.
[    0.000000] Entering idle loop.

Redis client

RESP encode/decode and 80+ commands, written against the wire protocol.

1,435 lines · 35 tests · 0 failing

WebDAV, RFC 4918

An XML layer, a client (PROPFIND, MKCOL, MOVE, COPY…) and a server.

971 lines · 99 tests · 0 failing

Sond, in Sond

The compiler's own lexer, ported from the Rust implementation: the first step to self-hosting.

506 lines · 39 tests · 0 failing

An 8-bit microcontroller

The same compiler emits Intel HEX for a PIC16F684: 2 KB of flash, 128 bytes of RAM.

x86-64 kernel → 8-bit MCU, one language

Every figure above was produced by compiling the source and running the test binaries, not by asking the author. The libraries were written by small, inexpensive models working in a red→green loop against the compiler, with no Sond in their training data and nothing to go on but the language reference. That is not the selling point; it is the design constraint being met. If the proof burden were too heavy to discharge automatically, none of this would exist.

The compiler is the oracle.

Every function can carry a contract. sondc proves it against the body at compile time. A contract it cannot prove is a compile error, not a runtime surprise, not a failing test you forgot to write.

✓ Compiles the body proves the contract

// abs never returns a negative number.
fn abs(x: i64) -> (r: i64)
    ensures { r >= 0 }
{
    if x >= 0 { x } else { 0 - x }
}

✗ Rejected at compile time the body does not prove the contract

// Same promise, wrong body: x can be negative.
fn abs(x: i64) -> (r: i64)
    ensures { r >= 0 }
{
    x
}

error: postcondition not proven
  --> abs.snd
   |  ensures { r >= 0 }
   |           ^^^^^^^^ the prover cannot show this holds for every input
   = note: when x < 0, r = x < 0

Out-of-bounds indexing does not compile

Indexing is checked by default, at compile time. Write s[i] and the compiler must be able to prove 0 ≤ i < s.len from the loop condition, a precondition, or a branch guard. If it can't, the program is rejected.

The two functions on the right differ by one line. That line is the proof.

Nothing is checked at runtime, so there is no bounds-check to pay for and no panic to handle: the cost was paid once, in the compiler.

✗ Rejected

pub fn sum(s: Slice, n: i64) -> i64 {
    let mut total = 0
    let mut i = 0
    while i < n {
        total = total + s[i]
        i = i + 1
    }
    total
}

error: function `sum`: cannot prove this index
is in bounds for slice `s`; bound it with a
`where`/`requires`/loop condition to 0..s.len

✓ Compiles one line of proof

pub fn sum(s: Slice, n: i64) -> i64
    requires { n <= s.len }
{
    // ...unchanged...
}

“But what about a value that only exists at runtime?”

It is the first question everyone asks, and it has a precise answer. A proof is not a test over sample values: it is universally quantified over every input, which is why the compiler can hand you the counterexample.

Obligations do not stop at the function. They travel to the caller: pass an unproven value and the caller is rejected.

At the edge of the program (a byte off the wire, a sensor, argv), nothing can be proven statically. So the compiler makes you write the check exactly there, once. That is the real claim: not that runtime checks disappear, but that they are forced at the boundary and provably unnecessary everywhere inside.

pub fn caller(y: i64) -> i64 {
    needs_positive(y)   // y may be negative
}

error: contract violation: function `caller`:
cannot prove the precondition `y >= 0` required
when calling `needs_positive`
(counterexample: y = -1)

✓ Compiles the check the compiler forced

pub fn caller(y: i64) -> i64 {
    if y >= 0 { needs_positive(y) } else { 0 }
}

Divide-by-zero is a compile error

Sond proves the divisor is non-zero before it lets you divide. No runtime crash, no defensive check you might forget, and when it refuses, it names the value that breaks you.

// ✗ rejected: divisor not proven non-zero
fn ratio(a: i64, b: i64) -> i64 {
    a / b
}

// ✓ accepted: precondition proves b != 0
fn ratio(a: i64, b: i64) -> (r: i64)
    requires { b != 0 }
{
    a / b
}

Illegal states don't compile

A variant can carry a payload, and the only way to read it is match, which forces you to handle the empty case. The billion-dollar mistake, forgetting to check for absence, is unrepresentable rather than discouraged.

Enums are concrete, not generic: you declare the Opt you need. Generics are not in the language yet.

enum Opt { Some(i64), None }

// Can't divide by zero: returns None.
pub fn safe_div(a: i64, b: i64) -> Opt {
    if b == 0 { None } else { Some(a / b) }
}

// You must handle None to reach the value.
pub fn unwrap_or(o: Opt, fallback: i64) -> i64 {
    match o {
        Some(x) => x,
        None => fallback,
    }
}

From a contract to the metal, and down to 8 bits

Sond has no interpreter and no runtime. sondc emits a hosted ELF, a libc-free /init, a UEFI application that boots with no OS underneath, and Intel HEX for a PIC16F684, a microcontroller with 2 KB of flash.

The same proven language runs the x86-64 kernel above and an 8-bit chip that costs less than a coffee.

$ sondc app.snd -o app            # hosted ELF
$ sondc init.snd --freestanding   # libc-free /init
$ sondc boot.snd --uefi           # BOOTX64.EFI, bare metal
$ sondc blink.snd --pic16         # Intel HEX, 8-bit MCU

“Isn't this just Dafny?”

Proving contracts at compile time is not a new idea: Eiffel named require/ensure in 1986, and Dafny, SPARK and F* have done it well for years. Here is the honest position against each neighbour, including where they win.

vs. Dafny · SPARK · F*

They win: far more powerful proof systems. Sond's prover is linear arithmetic; theirs reach where Sond cannot follow.

Sond has no external solver: no Z3, no separate verification pass, zero dependencies. Proving is compiling. And none of them boots on bare metal from its own backend; they emit C#, Java, Go, or C.

vs. Rust

It wins: ecosystem, maturity, tooling, and a decade of production use. For anything you ship this year, use Rust.

Rust's index safety is a runtime check that panics. Sond's is a compile-time proof: no check to pay for, no panic path to handle, which matters most exactly where Rust is least comfortable, with no allocator underneath.

vs. C

It wins: it is everywhere, and it will outlive all of us.

In C's own territory (kernels, firmware, microcontrollers, no runtime), its answer to the buffer overflow is still “be careful”. Sond's is a proof, at the same cost: none.

Where this is going, stated as a bet rather than a fact: the gap worth occupying is Rust's guarantees without the borrow checker, and Go's simplicity without the garbage collector. Sond reaches that only if dynamic memory can be made safe with neither a collector nor lifetime annotations. That design is open, and it is the question the project lives or dies on, not a solved problem being marketed as one.

Install Sond

No root required. Installs sondc, the standard library, and the language reference.

curl -fsSL https://sond.dev/install.sh | bash

curl -fsSL https://sond.dev/install.sh -o install.sh
less install.sh          # read it before you run it
bash install.sh

git clone https://github.com/fredyk/sond
cd sond
cargo build --release --manifest-path compiler/Cargo.toml
tools/install.sh

Installs sondc to ~/.local/bin, the standard library to ~/.local/lib/sond, and the language reference Sond.md to ~/.local/share/sond. Requires git and a Rust toolchain (cargo). Then: man sondc · man sond · language reference.

Open source. Real compiler. Honest about the gaps.

Apache-2.0 github.com/fredyk/sond

A real compiler in Rust, built bottom-up with strict TDD: a linear-arithmetic prover with path-sensitive branches, inter-procedural contract summaries, loop invariants and interval-based bounds analysis. Payloaded enums. Four backends: hosted, freestanding, UEFI and PIC16.

Not there yet: generics, full effects and capabilities, a package manager, formal versioning. Integer overflow is checked for constants and can be opted out of per function with wrapping fn, but the language-wide flip is still blocked on richer types: measured, attempted, and reverted rather than shipped half-proven. It is an active experiment, not a finished product.

Rust's guarantees without the borrow checker. Go's simplicity without the garbage collector.