A formalization of the CHERIoT+RTOS model.
The abstract model is in src/Spec.v, various validation lemmas and corollaries are in src/SpecLemmas.v, and properties about the system are in src/Properties.v.
This project depends on Rocq.
-
Notifications
You must be signed in to change notification settings - Fork 0
A formalization of the CHERIoT+RTOS model
License
Cherified/cheriot-abstract-spec
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
A formalization of the CHERIoT+RTOS model
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published