Nitpick Design by Contract and Formal Verification

Nitpick is distinct from other bare-metal languages because it ships with formal mathematical verification integrated directly into its compiler pipeline, powered by the Z3 SMT solver. This enables you to prove your code’s correctness at compile time, matching the safety guarantees of languages like Ada/SPARK.

1. Value Constraints: limit<Rules>

Nitpick allows you to define constraints on value ranges called Rules. You can then bind these rules to variables using the limit<RuleName> syntax.

// 1. Define a rule for an integer
Rules<int32>:r_positive = { $ > 0i32 };

func:main = int32() {
    // 2. Bind the rule to a variable
    limit<r_positive> int32:x = 5i32;
    exit 0i32;
};

When you compile with --verify, the compiler’s integrated Z3 solver will mathematically prove that the assigned value (5i32) satisfies the constraint ($ > 0). If it cannot prove it statically (for instance, reading user input), it will enforce the check at runtime. If the runtime check fails, it triggers the failsafe handler.

2. Function Contracts: requires and ensures

Nitpick implements classic Design by Contract (DbC) on function boundaries.

• requires: Preconditions that must be true when the function is called.
• ensures: Postconditions that the function guarantees will be true when it returns. (Use the special result keyword to reference the return value).

func:divide = int32(int32:a, int32:b) 
    requires b != 0i32 
    ensures result > 0i32 
{
    pass 10i32; // Hardcoded for example
};

2.1 Static Verification vs Runtime Enforcement

When you compile with the --verify-contracts flag, the compiler translates these contracts into Z3 assertions to prove they are mathematically valid. Currently, the compiler verifies that the contracts are individually satisfiable.

If you don’t use the static verifier, Nitpick automatically enforces these contracts at runtime.

2.2 The Result<T> Intercept

One of the most powerful features of Nitpick’s DbC implementation is how it interacts with the type system. If a function declares a requires clause, Nitpick implicitly changes its return type to a Result<T>.

If a caller violates the precondition at runtime, the function immediately intercepts execution and returns a Result error rather than crashing or triggering the failsafe. This heavily intertwines contract programming with Nitpick’s sticky error propagation system, forcing the caller to explicitly unwrap or handle potential contract violations using raw, drop, or .is_error.

func:main = int32() {
    // Because `divide` has a `requires` contract, it returns a Result<int32>!
    // We must unwrap it with `raw` or handle the potential failure.
    int32:y = raw divide(10i32, 2i32);
    
    exit 0i32;
};