CRYPTOGRAPHY / FORMAL METHODS
PEEL
A small F* experiment in labeled cryptographic expressions and a recorded path to C.
- Current state
- Research prototype
- Discipline
- Cryptography · Formal methods
- Built with
- F* / KaRaMeL / Z3 / OCaml / C
The idea
PEEL narrows the language question to one inspectable experiment: how can public and secret values be represented so that forbidden observations are rejected by the type system?
How it works
Two F* modules define classification labels and label-indexed bytes. Positive and expected-failure examples exercise the boundary. Pinned F*, Z3 and KaRaMeL tools verify and extract the byte-XOR subset, with scripts recording the resulting evidence.
What’s implemented
- Public/Secret labels with explicit join laws
- Label-indexed byte XOR and restricted public observation
- Expected verifier rejections and a scripted verification/extraction path
PROJECT STATUS / RESEARCH PROTOTYPE
Where it stands
P0 research prototype
- P0 research prototype; no custom PEEL parser
- The checked experiment is narrow and depends on its recorded toolchain
- No claim of cryptographic security, constant-time behavior or production readiness
Source & resources
GitHub repositorySource code and project documentation ↗SemanticsOpen resource ↗Trust boundaryOpen resource ↗
Documentation behind this project page
Reviewed October 1, 2026. Project descriptions reflect a source review; repository validation claims were not independently reproduced.