Verification

We formally verify Islet using Kani's model checking. Our verification harnesses adopt the same input and output conditions as well as similar structures used in TF-RMM's harnesses which are extracted from Machine Readable Specification. It would help to check the conformance of the two systems written in different languages.

Verification dependency

• patched Kani

Available RMI targets

rmi_features
rmi_granule_delegate
rmi_granule_undelegate

Verifying Islet

(in islet/model-checking)

# Choose one among the list in `Available RMI targets` for the value of `RMI_TARGET`
$ RMI_TARGET=rmi_granule_undelegate make verify