method Max(a: int, b: int) returns (m: int) ensures m >= a && m >= b ensures m == a || m == b { if a >= b { m := a; } else { m := b; } } predicate Sorted(s: seq<int>) { forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j] } method BinarySearch(a: array<int>, key: int) returns (index: int) requires Sorted(a[..]) ensures 0 <= index ==> a[index] == key ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key { var lo, hi := 0, a.Length; while lo < hi invariant 0 <= lo <= hi { var mid := (lo + hi) / 2; if a[mid] < key { lo := mid + 1; } else if key < a[mid] { hi := mid; } else { return mid; } } return -1; } lemma MaxCommutative(a: int, b: int) ensures Max(a, b) == Max(b, a) { }

fn verify(x: &State) -> bool { x.balance >= 0 && x.locked <= x.balance } #[requires(n > 0)] #[ensures(ret >= n)] fn next_pow2(n: u64) -> u64 { let mut p = 1; while p < n { p <<= 1; } p } (declare-const x Int) (declare-const y Int) (assert (> x 0)) (assert (= (+ x y) 10)) (check-sat) ; sat (get-model) ; (define-fun x () Int 3) ; (define-fun y () Int 7) (assert (forall ((a Int) (b Int)) (=> (and (> a 0) (> b 0)) (> (+ a b) 0)))) (check-sat) ; unsat impl Repair for Patch { fn verify(&self) -> Outcome { if self.tests_pass() && self.no_regression() { Outcome::Plausible } else { Outcome::Rejected } } }

Martin Mirchev

Portfolio

Formally Verifying nanoda

Frama-Clang

Contributions to Verus

ChatAFL

Cerberus

ANTLRStudio

Kernel