sabi: formal verification framework for Rust programs (including unsafe)

Dependency

• Isabelle 2020

The theory depends on Simpl, an imperative programming language for formal verification developed in Isabelle. The vendored version is taken from AFP-2020-06-03.

How to develop

Building sessions

Run the following command in the root directory (the directory with ROOT file):

$ isabelle build -d ./Simpl -D . -v

Launching a jEdit session

$ isabelle jedit -d ./Simpl -d . Rustv/Rustv.thy

The -l option seems to have Isabelle cache the Simpl heap:

$ isabelle jedit -l Simpl -d Simpl -d . Rustv/Rustv.thy