Tiny

Tiny is a small, statically typed, contract-based programming language for teaching formal verification. It feels like a simplified combination of Python and Dafny: ordinary imperative programs, plus requires / ensures contracts, assert, loop invariants, decreases termination measures, old(...), and forall / exists quantifiers. Verification is fully automatic: Tiny translates each program into verification conditions and asks the Z3 SMT solver to check them. There are no interactive proof tactics and no handwritten SMT formulas.

A program that verifies looks like this:

fn abs(x: Int) -> Int
  ensures result >= 0
{
  if x >= 0 {
    return x;
  } else {
    return -x;
  }
}

fn main() -> Int
{
  return abs(-7);
}

Running the verifier prints VERIFIED; running the program prints nothing and uses main's return value as the process exit code.

Installation

Tiny requires:

• Python 3.13 or newer, and
• the Python z3 bindings (z3-solver).

1. Install the Z3 Python bindings

uv venv
source .venv/bin/activate
uv add z3-solver

2. Install Tiny

From this directory:

uv pip install -e .

This installs a tiny command on your PATH. You can also run Tiny without installing it, using the module form:

python3 -m tiny check examples/abs.tiny

Usage

Tiny exposes three subcommands.

tiny check FILE.tiny

Parse, type-check, and verify the program. Prints VERIFIED on success, or FAILED/UNKNOWN with source locations on failure.

tiny run FILE.tiny

Type-check the program (without static verification) and execute main(). The exit status is main's return value.

tiny verify-run FILE.tiny

Verify first, and then execute main() if verification succeeded.

The language

Types

Tiny has three basic types:

Int          arbitrary-precision integers (no overflow)
Bool         true or false
String       a sequence of characters, written in double quotes

Tiny supports homogeneous one-dimensional arrays:

Array<Int>    mutable, fixed-length, zero-indexed arrays
Array<Bool>   mutable, fixed-length, zero-indexed arrays
Array<String> mutable, fixed-length, zero-indexed arrays of strings

Nested arrays (Array<Array<Int>>) are not allowed, and Tiny does not (yet) have a mapping (dictionary) type.

Functions

fn max(a: Int, b: Int) -> Int
  ensures result >= a
  ensures result >= b
  ensures result == a or result == b
{
  if a >= b {
    return a;
  } else {
    return b;
  }
}

• requires clauses are assumptions about the caller's inputs.
• ensures clauses are guarantees about the result.
  • result names the return value.
  • old(e) refers to the value of e at function entry.
• Multiple requires/ensures clauses are implicitly ANDed.
• A function may omit -> TYPE, making it a void procedure:

fn increment_first(a: Array<Int>)
  requires length(a) > 0
  ensures a[0] == old(a[0]) + 1
{
  a[0] = a[0] + 1;
}

• Recursive functions must declare a decreases measure.

Statements

let NAME: TYPE = expr;       // local variable declaration
NAME = expr;                 // scalar assignment
a[i] = expr;                 // array element assignment
if expr { ... } else { ... } // conditional (else optional)
while expr
  invariant expr             // loop invariants (optional)
  decreases expr             // termination measure (optional)
{ ... }
return expr;                 // (value-returning functions only)
assert expr;                 // runtime + static assertion
f(args);                     // procedure call statement

Expressions

Operators, from lowest to highest precedence: =>, or, and, ==/!=, </<=/>/>=, +/-/++, *///%, unary !/-/`, then indexing and calls.

/ and % use Euclidean integer division compatible with Z3 (the remainder is always non-negative). Division and modulo by zero are runtime errors and verification obligations.

String literals are written in double quotes and support the usual C-style backslash escapes (\n, \t, \", \\, and so on). The ++ operator concatenates two strings, and a single backtick before a value converts it to a string (5 is "5", x is the string form of x's value):

let greeting: String = "hello" ++ " " ++ "world";
let n: Int = 42;
let label: String = `n;  // "42"

Quantifiers are available in specifications:

forall i: Int :: 0 <= i and i < length(a) => a[i] >= 0
exists i: Int :: 0 <= i and i < length(a) and a[i] == 0

length(a) is the single built-in function.

Examples

The examples/ directory contains small programs:

• abs.tiny, max.tiny, count.tiny: the core required examples.
• required.tiny: all three core examples plus a main.
• factorial.tiny: recursive function with decreases.
• all_nonnegative.tiny: array property proved with a quantifier loop invariant.
• increment_first.tiny: a procedure mutating an array, with old.
• bad.tiny: a deliberately unprovable postcondition (FAILED).
• precondition.tiny: a runtime precondition violation.

Try them:

tiny check examples/required.tiny
tiny verify-run examples/factorial.tiny
tiny check examples/bad.tiny
tiny run examples/precondition.tiny

Intentional limitations

These choices keep the verifier sound and the implementation small; they match the specification's own "simplest recommended model":

Arrays are references, not values. : let b: Array<Int> = a; (array-to-array assignment) is rejected to avoid aliasing ambiguity. Create fresh arrays with array literals instead.

Functions return Int or Bool. : Array-returning functions are not supported. Array mutation is expressed with procedures, as shown earlier.

A call that takes array arguments must appear on its own. : It may be a statement, or the whole right-hand side of, let, return, or assignment. It may not be nested inside a larger expression (f(a) + g(a) is rejected during verification).

Runtime quantifier checking is best-effort. : Quantified postconditions over a finite array index range (0 <= i and i < length(a)) are evaluated at runtime. Other quantified expressions are skipped during runtime checking but still fully verified statically.

The verifier never claims success on a program it cannot prove. If Z3 cannot decide an obligation it reports UNKNOWN, and a genuinely unprovable program is reported as FAILED: it is never silently accepted.

Project layout

tiny/
  errors.py       error types and source-location formatting
  lexer.py        tokenizer
  parser.py       recursive-descent parser -> AST
  ast_nodes.py    AST node definitions
  types.py        Int / Bool / Array<T> types
  typechecker.py  name resolution + static type checking
  interpreter.py  concrete executor with runtime checks
  prover.py       verification-condition generation + Z3 proof checking
  cli.py          the `tiny` command-line interface