Prusti

Aliases: —

Provenance: commit 6b3ee6e555 · authored 2026-03-16T22:31:52+01:00 · agent claude-code · model claude-sonnet-4-6

1 source · not in taxonomy (canonical name didn't match any upstream)

Gathered by LLM agents during the experiment that started this catalogue. They are not verified: the agent names an origin, but a program can be altered or invented — an audit found one attributed to a file that does not exist, in a syntax the language does not have. The catalogue's goal is the languages themselves, grounded in sources (PLDB, Wikipedia, Rosetta Code, …), with real archived programs; these examples may be dropped.

use prusti_contracts::*;

#[ensures(result >= a && result >= b)]
#[ensures(result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
    if a < b {
        b
    } else {
        a
    }
}

#[requires(n >= 0)]
#[ensures(result == n)]
fn identity(n: i32) -> i32 {
    n
}

fn main() {
    let m = max(3, 7);
    assert!(m == 7);
    let m2 = max(5, 2);
    assert!(m2 == 5);
}