Formal Methods Techniques

Contract systems

Racket’s contracts are checked at run time (dynamic)
- Some work on “soft contracts” that try to statically eliminate those that can be proved correct for all inputs
Typical Racket contracts check basic type-like facts e.g. “is number”
However, they do also support arbitrary predicates, similar to other general contract systems

Rosette seems to be more like a solver-aided DSL toolbox for verification, synthesis, etc.
PLDI 2014 paper has useful context comparing symbolic execution, bounded model checkers, and finally their own approach
Possible to build contract-style verifiers (among others) but hasn’t been done yet for Lisp family languages with Rosette
Serval builds on Rosette to create automated verifiers for various ISAs

Also called “deductive program verification” by Why3 and related tools
Formal verification of functional correctness
- Typically achieved by annotating pre and post conditions (contracts)
- Some also check for termination as well
Complex to achieve this with traditional imperative languages like C, Java, etc.
- Creusot leverages Rust’s borrow checker escape such troubles
Several different contract verification tools for Rust
- Rust’s lang team is exploring some kind of standardised contract language
- Creusot focuses on functional correctness, seems to have a smart overall design
- Prusti verifies functional correctness plus ownership (that Rust compiler already checked), can take 100x eval time vs. Creusot, struggles with some concepts like reborrowing in a loop
- Aeneas translates to “low-level borrow calculus” and then applies F*, currently behind Prusti and Creusot on language support
- Verus is similar to Creusot, with added feature of “linear ghost permissions” which allow verifying raw pointer accesses