Formal Verification

from types to theorems

Why This Matters

Testing shows bugs exist. Proof shows they don't. Space makes memory bugs impossible — if it compiles, they don't exist.

Testing vs. Proof

Testing shows that a program works for specific inputs. Proof shows that a program works for all inputs.

Approach	Guarantee	Coverage
Manual testing	Works for cases I tried	Dozens of cases
Unit tests	Works for cases I wrote	Hundreds of cases
Property tests	Works for random cases	Thousands of cases
Fuzzing	Works for adversarial cases	Millions of cases
Proof	Works for all cases	Infinite cases

This isn't a difference of degree. It's a difference of kind. A million test cases still leave infinitely many untested. A proof leaves none.

The Verification Stack

Space achieves verified correctness through a chain of tools, each building on the last:

Space source code
↓
Space Compiler (written in SPARK)
↓
Generated SPARK code with contracts
↓
GNATprove (verifies proofs via Z3/Alt-Ergo/CVC4)
↓
GNAT → native binary (bare metal capable)

SPARK

SPARK is a formally verifiable subset of Ada, designed for high-integrity systems. It has been used in aerospace, rail, defense, and medical devices for over 30 years.

SPARK code includes contracts — preconditions, postconditions, and invariants that specify what the code must do. GNATprove verifies these mathematically. The Space compiler generates SPARK with contracts that encode Space's safety guarantees.

GNATprove

GNATprove is AdaCore's verification engine for SPARK. It translates SPARK code and contracts into the Why3 intermediate language, then uses SMT solvers (Z3, Alt-Ergo, CVC4) to discharge proof obligations.

When you write a contract, GNATprove asks: "Is there any execution path where this contract could be violated?" If the SMT solver proves no such path exists, the property is verified.

What Gets Proven

No runtime errors — No buffer overflows, no division by zero, no integer overflow
Contract compliance — Preconditions imply postconditions
Data flow correctness — No uninitialized reads, no data races
Functional correctness — Code does what the specification says

Bare Metal Capability

The Space compiler is itself written in SPARK. This enables:

On-target compilation — The compiler runs on the target hardware
Self-hosting — Can compile itself on bare metal
Zero dependencies — No OS, no runtime, no garbage collector
Minimal TCB — Smaller trusted computing base for certification

GNAT compiles to native code for Linux, macOS, Windows, and bare metal targets. The same verified code runs everywhere.

What Space Proves

The Space implementation includes machine-checked proofs of these properties:

Stack Correctness

The fundamental stack operations are verified:

Push then pop returns the original value
Size increases by one after push
Size decreases by one after pop (when non-empty)
Empty stack has size zero

GNATprove verifies these properties hold for all possible stack states — not just test cases.

Universe Isolation

Pointers are tagged with their universe of origin. You can only read from pointers belonging to the current universe — this is verified at compile time, not checked at runtime.

Cross-universe access requires explicit borrowing, which the verification also tracks. Pointers cannot escape their universe.

Discipline Compliance

Each discipline's rules are verified:

Linear — values must be consumed exactly once; universe must be empty when destroyed
Affine — values can be dropped but not copied
Unrestricted — values can be copied freely

Linear values carry a proof obligation: they must be consumed before the universe can be destroyed. GNATprove verifies this requirement is met.

Borrow Safety

Borrowed pointers track their source universe. The verification ensures:

Borrowed pointers must be dropped to end the borrow
Source universe can't be destroyed while borrows are active
Borrowed data can be read but not moved

A universe can only be released when all borrows have been dropped. This is verified at compile time, not runtime.

Unicode Correctness

Space includes complete Unicode 15.0 support with verified correctness:

UTF-8 encoding/decoding — proven well-formed
UAX #29 grapheme clustering — correct emoji and combining mark handling
NFC/NFD/NFKC/NFKD normalization — canonical equivalence preserved
Case mapping — 1450 uppercase, 1433 lowercase mappings

Most languages treat Unicode as a library concern. Space verifies it at the core — if your text operations compile, they handle all of Unicode correctly.

The SMT Connection

GNATprove doesn't prove everything manually. It delegates to SMT solvers: Z3, Alt-Ergo, and CVC4.

When you write a contract, GNATprove translates it into the Why3 intermediate language, then into logical formulas for the SMT solvers: "Is there any execution path where this contract could be violated?" If the solver finds a counterexample, compilation fails. If no counterexample exists, the property is verified.

This automation is crucial. Writing proofs by hand is tedious and error-prone. SMT solvers handle the mechanical parts, letting you focus on the interesting properties.

Trusted Computing Base

Every verified system has a trusted computing base (TCB) — the components you must trust to be correct, because they're not themselves verified.

Space's TCB is minimal:

Component	Trust Reason
GNATprove	Verifies proofs
SMT solvers (Z3, Alt-Ergo, CVC4)	Discharge proof obligations
GNAT compiler	Generates machine code
Hardware	Executes instructions

Notably absent: the Space compiler itself. Because Space generates SPARK code that GNATprove verifies, any compiler bug would be caught downstream. This architecture would make the Space compiler eligible for TQL-5 (lowest tool qualification level) under DO-178C — errors are detected by subsequent verification.

What Proofs Cannot Do

Proofs are powerful, but not omnipotent. They cannot guarantee:

Correct specification — Proofs verify that code matches its spec. If the spec is wrong, the code is wrong.
Termination — GNATprove can prove termination for many programs, but some valid programs have unprovable termination.
Hardware correctness — Proofs assume the CPU executes instructions correctly. Cosmic rays and hardware bugs are out of scope.
Side-channel resistance — Proofs about functional behavior don't cover timing attacks or power analysis.

Verification reduces the attack surface. It doesn't eliminate it entirely.

Verified vs. Certified

Space produces verified code, not certified code. These are different things:

Term	Meaning	Who Provides It
Verified	Proofs discharged, no runtime errors	Space + GNATprove
Certifiable	Suitable for certification process	Space + GNATprove
Certified	Approved by certification authority	Customer + DER

Space produces verified, certifiable code. Certification itself requires additional customer-provided artifacts: requirements traceability, test coverage (MC/DC), design documentation, compliance matrices, and approval by a Designated Engineering Representative (DER).

We reduce the cost of certification. We don't do certification.