Summary #

Verus overview

Getting started #

• Getting started
  • ... on the command line
  • ... with VS Code

Tutorial: Fundamentals #

• Using Verus within Rust
• Basic specifications
  • assert, requires, ensures, ghost code
  • Expressions and operators for specifications
  • Integers and arithmetic
  • Equality
• Specification code, proof code, executable code
  • spec functions
  • proof functions, proof blocks, assert-by
  • spec functions vs. proof functions, recommends
  • Ghost code vs. exec code
  • const declarations
  • Putting it all together
• Recursion and loops
  • Recursive spec functions, decreases, fuel
  • Recursive exec and proof functions, proofs by induction
    • Lightweight termination checking
  • Loops and invariants
    • Loops with break
    • For Loops
    • Iterators
  • Lexicographic decreases clauses and mutual recursion
• Datatypes: struct and enum
  • Struct
  • Enum
• Libraries
  • Specification libraries: Seq, Set, ISet, Map, IMap
  • Executable libraries: Vec
• Spec closures
• Quantifiers
  • forall and triggers
  • Multiple variables, multiple triggers, matching loops
  • exists and choose
  • Proofs about forall and exists
  • Example: binary search
  • Ambient (broadcast) lemmas

Tutorial: Proof Development #

• Developing proofs
  • Using assert and assume
  • Devising loop invariants
  • Proving absence of overflow
• SMT solving, automation, and where automation fails
  • What's decidable, what's undecidable, what's fast, what's slow <!--- Chris --->
  • Integers and nonlinear arithmetic
  • Bit vectors and bitwise operations
  • forall and exists: writing and using triggers, inline functions <!--- Chris --->
  • Recursive functions <!--- Chris --->
  • Extensional equality
  • Libraries: incomplete axioms for Seq, Set, Map <!--- Chris --->
• Managing proof performance and why it's critical
  • Measuring verification performance
  • Quantifier profiling
  • Modules, hiding, opaque, reveal
  • Hiding local proofs with assert (...) by { ... }
  • Structured proofs by calculation
  • Proof by computation
  • Spinning off separate SMT queries
  • Breaking proofs into smaller pieces
• Using LLM assistants
  • Using LLMs to develop proofs
  • Using LLMs to develop specifications
• Checklist: what to do when proofs go wrong

Tutorial: Verification and Rust #

• Mutation, references, and borrowing

  • Mutable references
  • Assertions about mutable references

• Traits

• Iterator Specifications

  • Finite Iterators
  • Infinite Iterators

• Higher-order executable functions

  • Passing functions as values
  • Closures

• Ghost and tracked variables

• Strings

• Macros

• Unsafe code & complex ownership

  • Cells / interior mutability
  • Pointers
  • Concurrency

• Logical atomicity

  • Atomic specifications
  • Invoking the linearization point
  • Calling a logically atomic function

• Verifying a container library: Binary Search Tree

  • First draft
  • Encapsulating well-formedness with type invariants
  • Making it generic
  • Implementing Clone
  • Mutable references in a container
  • Full source for the examples

• Interacting with unverified code

  • Calling unverified code from verified code
  • Calling verified code from unverified code

• Understanding the guarantees of a verified program

  • Assumptions and trusted components
  • Memory safety is conditional on verification
  • Calling verified code from unverified code

Installation, configuration, and tooling #

• Installation and setup

  • IDE Support
  • Installing and configuring Singular

• Project setup and development

  • Using Verus via Cargo
  • Documentation with Rustdoc
  • Ghost Erasure

Reference #

• Supported and unsupported Rust features
• Verus syntax by example
• Modes
  • Function modes
  • Variable modes
• Contributed Extensions
  • Automatic spec to exec functions
  • Spec and proof attributes for exec functions
    • Automatic exec to spec functions
• Specification language
  • Type Interpretations
  • Spec expressions
    • Operator Precedence
    • Rust subset
    • Arithmetic
    • Bit operators
    • Coercion with as
    • Spec equality (==)
    • Extensional equality (=~=, =~~=)
    • Prefix and/or (&&& and |||)
    • Chained operators
    • Implication (==>, <==, and <==>)
    • Quantifiers (forall, exists)
    • Such that (choose)
    • Trigger annotations
    • The view function @
    • Spec index operator []
    • The has operator
    • The is operator
    • The matches operator
    • decreases_to!
• Proofs
  • Proof statements
    • assert
    • assume
    • assert ... by
    • assert forall ... by
    • assert ... by(...)
    • reveal, reveal_with_fuel, hide
    • reveal_strlit
  • Prover modes
    • "default" mode
    • bit_vector
    • nonlinear
    • integer_ring
    • compute/compute_only
• Function specifications
  • Function Signatures
    • Exec fn signature
    • Proof fn signature
    • Spec fn signature
  • Signature clauses
    • requires / ensures
    • returns
    • opens_invariants
    • no_unwind
    • recommends
  • Traits and signature inheritance
  • Specifications on FnOnce
• External trait specifications
• Loop specifications
  • invariant
  • invariant_except_break / ensures
• Recursion and termination
  • decreases ... when ... via ...
  • Datatype ordering
  • Cyclic definitions
• Type invariants
• Attribute list
• Directives
  • assume_specification
  • global
• Misc. Rust features
  • Statics
  • Unions
  • Pointers and cells
• Command line
  • --record
• Planned future work