Pre-alpha · solo · cryptography
Orange
Cryptography you can check.
Abstract
A language and toolchain for specifying, implementing, and verifying cryptography — so mathematical intent, native code, and assurance evidence stay connected instead of living in separate tools.
Inside No Such Machine’s cryptography and signals work, Orange is the language track: keep mathematical intent, executable realization, and assurance evidence connected instead of scattered across unrelated tools. Claims stay narrow; evidence is meant to be replayed.
Limits. Pre-alpha and solo-built. The compiler checks and evaluates a typed fragment. It does not yet generate native code or check proofs. Nothing in the repository has been independently reviewed or formally verified.
Example
Fragment the current compiler accepts — SHA-256 helpers from FIPS 180-4, written the way the standard writes them.
edition 2026;
module sha256 {
spec choose(x: Word[32], y: Word[32], z: Word[32]) -> Word[32] {
(x & y) ^ (~x & z)
}
spec majority(x: Word[32], y: Word[32], z: Word[32]) -> Word[32] {
(x & y) ^ (x & z) ^ (y & z)
}
}References
- Repository
- Source tree, fixtures, and toolchain.
- The Orange Book
- Living reader guide for intent, status, and open questions.
- Orange School
- Competency path from no assumed background into the language.
