Formal verification (Formal Silk)

Silk includes syntax for writing contracts and verification metadata:

• #require / #assure for pre/postconditions
• #assert for local assertions
• #invariant / #variant / #monovariant for loops

Full reference: formal verification.

Example (Design / verifier-oriented)#

#require x >= 0;
#assure result == x + 1;
fn inc (x: int) -> int {
  return x + 1;
}

See also#

• Full reference: formal verification