Prusti
1 program
Added 2026-03-16T10:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 6b3ee6e555 · authored 2026-03-16T22:31:52+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Verified max and identity functions
Provenance: commit 6b3ee6e555 · authored 2026-03-16T22:31:52+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
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);
}