FORMAL METHODS / SYSTEMS / SECURITY GOVERNANCE
SEAL
A small F* authority model that makes capability, evidence and receipt requirements explicit.
- Current state
- Formal-model prototype
- Discipline
- Formal methods · Systems / security governance
- Built with
- F* / Low* direction / Make / GitHub Actions
The idea
An authority decision should reveal which capability, evidence and receipt it requires. SEAL models that decision as a small fail-closed gate whose allowed outcomes can be checked against explicit invariants.
How it works
Typed subjects, operations, policies, evidence and receipt states feed a total F* decision function. Lemmas express that an allowed decision implies the required capability and supporting state; an explicit decision matrix records check precedence and denied combinations.
What’s implemented
- Capability-first total authorization gate
- Evidence requirements for open, seal and transition operations
- Receipt requirement for transitions
- F* lemmas and explicit operation decision matrix
- Repository F* verification workflow
PROJECT STATUS / FORMAL-MODEL PROTOTYPE
Where it stands
Formal-model prototype
- SEAL-Core v0 is a narrow authority model with no parser; example files are documentation fixtures
- C extraction is deferred until a compatible KaRaMeL toolchain is pinned
- Kernel isolation, seL4 equivalence, production authorization and whole-system formal verification are not established
Source & resources
Documentation behind this project page
Reviewed October 1, 2026. Project descriptions reflect a source review; repository validation claims were not independently reproduced.