How it works

The program proved
is the program compiled.

Three syntaxes reach one abstract syntax, one semantic analysis and one intermediate representation, Byron Core. Flow analysis, the prover, the reference interpreter and the LLVM code generator all read that same Core, and the prover's results decide which checks the generated code still makes.

The pipeline

Noel

.ads · .adb

lexer → parser

Leon

.leon

lexer → parser → names → extract

Leno

.py

lexer → parser → desugar → as Leon

Shared AST

Below this point nothing knows which syntax a unit was written in.

Semantic analysis

Names resolved, types checked, Ada's legality rules applied: a typed tree.

Byron Core

Structured control flow, every run-time check explicit, contracts as data.

Flow analysis

Initialisation, Global and Depends, ownership, aliasing, elaboration, ghost code, tasking, termination.

Prover

Verification conditions, static discharge, cache, certificates, Z3 with cvc5 and Yices as fallbacks, counterexamples and advice.

Interpreter

Replays counterexamples, proposes loop invariants from real runs, and is the test suite's oracle for native code.

Code generator

LLVM: object files and a native link, or a JIT for run and the REPL.

The prover's set of proved checks flows to the code generator: a proved check produces no code at all.

Byron Core

One representation
for every engine.

Lowering turns every Ada rule Core does not know into something it does: checks become explicit, 'Old becomes a snapshot, a callee's precondition becomes a check at each call. What's left is small enough for every engine to agree on, and byronic emit --emit core writes it out as text.

Structured control flow

if, loop, exit, return, raise and handled blocks. No gotos and no basic blocks: case statements, while and for loops and short-circuit forms have all been lowered to these.

Explicit checks

Every run-time check Ada makes is a check statement with a kind, a condition, a span and a message. Nothing inside an expression checks anything.

Mathematical expressions

Expressions have no side effects, and arithmetic means the mathematical result. Whether it fits is the job of a check placed before it is used.

Contracts as data

Preconditions, postconditions, 'Old snapshots, flow contracts, variants and exceptional cases are fields of a subprogram, not statements in its body.

The prover

Fast, repeatable,
and honest about failure.

One verification condition per check, assertion, invariant step, variant and postcondition, generated by symbolic execution over Core's structured control flow and spread over parallel solver sessions.

Static discharge

Interval reasoning settles many range and overflow checks before a solver is asked.

Deterministic budgets

Solver effort is counted in resource units, never time, so a proof that passes on your laptop passes in CI, with any number of parallel sessions.

A proof cache

Each decided condition is keyed by the SHA-256 of its SMT-LIB text, so a second run proves only what changed.

Certificates

The unsat core behind each proof, in sorted text files you commit. Another machine re-checks each core without searching again.

Definite counterexamples

A failure is called definite only when the solver's values, replayed on the interpreter, reach the failing check.

Invariant candidates

When a loop invariant is too weak, the loop's states on real runs suggest stronger ones, kept only if they prove.

Code generation

Native code with nothing left to check

Ordinary code computes in machine widths, which is exact because its checks were proved. In an advisory build, an unproved check becomes a branch to the run time that reports the same code, place and message the prover would have. Exceptions use status returns, not an unwinder, and the C run time is static, with no garbage collector. Tasks and protected objects run on POSIX threads.

byronic build caches an object file per unit and links with the system C compiler. byronic run and the REPL use a JIT, running each program on a guarded thread so that a failed check returns to the compiler instead of ending it.

Checked against the originals

GNAT, GNATprove and CPython as oracles

Every legal Byron program is legal Ada, so Byron's test suite holds itself to the existing tools: every corpus passes GNAT's syntax check, programs built with GNAT print what Byron's do, GNATprove proves the same corpora, and each Leno program prints what CPython prints. Every corpus is also translated between the three syntaxes and back, and must lower to the same Core.

Byron itself is written in Haskell, on LLVM and Z3. Everything it links or ships carries a permissive licence.