History

Rafal Kolanski 1ab65b78ed refine+crefine: arch-split Machine_R Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>		2025-07-08 15:05:33 +10:00
..
access-control	arm access+infoflow: SGISignalCap security thms	2025-07-07 08:53:07 +10:00
asmrefine	isabelle2021-1: remove no_take_bit	2022-03-29 08:38:25 +11:00
bisim	arm proof: update for det_ext refactor	2025-05-01 10:55:20 +10:00
capDL-api	capDL-api: seplogic lemmas for ARMIssueSGISignal	2025-07-07 08:53:07 +10:00
crefine	refine+crefine: arch-split Machine_R	2025-07-08 15:05:33 +10:00
dpolicy	drefine+dpolicy: SGISignalCap proofs	2025-07-07 08:53:07 +10:00
drefine	drefine+dpolicy: SGISignalCap proofs	2025-07-07 08:53:07 +10:00
infoflow	riscv infoflowc: SGISignalCap update	2025-07-07 08:53:07 +10:00
invariant-abstract	arm+arm-hyp+aarch64 ainvs: SGISignalCap proofs	2025-07-07 08:53:07 +10:00
refine	refine+crefine: arch-split Machine_R	2025-07-08 15:05:33 +10:00
sep-capDL	capDL: add SGISignalCap API to capDL	2025-07-07 08:53:07 +10:00
Makefile	proof/Makefile: declare InfoFlowCBase dependencies	2024-07-05 18:03:59 +10:00
README.md	license: provide documentation under CC-BY-SA-4.0	2020-03-16 14:19:15 +08:00
ROOT	proof/ROOT: update comment for RefineOrphanage session for newer arches	2024-03-26 09:33:34 +01:00
tests.xml	regression: increase CRefine timeout	2020-11-26 00:31:04 +11:00

Formal Proofs about seL4

This directory contains the formal proofs about seL4, which mostly prove properties about the various seL4 specifications.

Each such proof lives in its own subdirectory: