A formal verification tool with the following features:

• DSL for writting proofs supported by F#'s computation expressions
• Z3 as inference engine
• Extraction of proof obligations from several languages
• Cross-language proofs: semantics can be extracted from different languages and combined to prove theorems about the whole project

Features and progress

• Check proofs written in a syntax inspired by Dijkstra's predicate calculus

  • A Logical Approach to Discrete Math
    • Prove properties with booleans, integers, sequences and functions GriesSchneider.fs
  • Relational calculus

• Extract proof obligations from

  • Rust
  • F#
  • Golang
  • Compact
    • Compact modules
    • Compact demo
  • Wybe, a language inspired by Dijkstra's Guarded Command Language

Installation instructions

• Install the dotnet 10 CLI
• Clone this repository locally

Example proof