Cryptographic software is asked to carry several different meanings at once. It has a mathematical meaning: a function, construction, or protocol is being described. It has an operational meaning: instructions execute on concrete machines with finite words, memory, errors, and timing behavior. It has a security meaning: an attacker is granted certain powers and a property is claimed under stated assumptions. Finally, it has an evidentiary meaning: some combination of proofs, certificates, tests, reviews, provenance, and build records is supposed to justify what users are told.
Those meanings rarely live in one place today. A specification may be written in a notation suited to mathematicians. A fast implementation may be C, Rust, or assembly. Functional correctness may be argued in a proof assistant. Constant-time behavior may be checked by a separate analysis. Game-based security may use yet another formalism. Test vectors, compiler flags, linker inputs, target features, and release attestations collect around the outside.
Each tool can be excellent. The difficulty is the crossings between them.
Six questions for one artifact
Imagine receiving a native library that exports a cryptographic routine. A serious account of that library should answer at least six questions:
- What mathematical construction or protocol component is intended?
- Which executable implementation is claimed to realize it?
- Which properties are claimed, for which inputs, targets, and versions?
- Which assumptions and leakage model limit each property?
- Which proof object, checked certificate, test corpus, or external record supports each claim?
- Which source, toolchain, dependencies, and invocation produced the shipped bytes?
It is possible to have good answers to several of these questions and no reliable answer to the next one. A proof about a mathematical function does not identify the binary loaded by an application. A correct implementation at one intermediate representation does not establish that a later optimization kept its behavior. Passing official vectors does not cover all inputs. Source-level control-flow discipline does not automatically describe final machine-code leakage. A reproducible build faithfully reproduces a bug just as readily as a correct program.
The transition is therefore part of the claim. Serialization is not merely plumbing when a theorem fingerprint can be attached to the wrong definition. Foreign-function glue is not merely plumbing when buffer length, aliasing, alignment, or error behavior can violate a proved precondition. The compiler is not merely plumbing when the advertised property must survive to object bytes. The release process is not merely plumbing when an attacker can replace either the code or its evidence.
The seams are part of the system.
The proposed vertical artifact
Orange’s directed mission is to specify, implement, and verify cryptography. The project’s proposed answer to the seam problem is a claim-oriented language and build graph. In the intended end state, a package connects standards provenance, readable specifications, executable implementations, named target and leakage models, checked transformations, native artifacts, foreign-interface metadata, tests, and explicit assumptions.
The important word is connects. Orange is not useful merely because it can place several kinds of text in one source file. A shared spelling is not a semantic relationship. The system must preserve exact identities and record which checked step supports each edge of the graph. Where a relationship has not been established, the graph must say so.
This is why the long-term product is larger than a notation or compiler front end. A language can make intent expressible, but an assurance claim also needs semantics, checking rules, artifact identity, assumptions, and replay. A code generator can produce fast bytes, but speed says nothing about whether those bytes implement the named specification. A theorem prover can check a proof, but the theorem may not be the property an integrator thinks it is.
Many architectural details of this vertical artifact remain proposed or under investigation. The current Typed Reference Core for literal specifications has no canonical encoding, proof identity, or refinement role and does not select the complete semantic Core. Orange has also not selected its proof foundation, proof format, solver policy, leakage baseline, native target envelope, stable foreign boundary, package model, or flagship cryptography corpus. This chapter describes the problem those choices must eventually solve; it does not settle them.
Claims, not labels
The word verified compresses too much. It can refer to well-formed syntax, memory safety, functional refinement, standards conformance, termination, constant-time behavior under a particular observation model, compiler preservation, ABI correctness, game-based security, or simply the fact that tests were run. These properties are related, but none is a universal substitute for the others.
Suppose a routine passes every published vector for a standard. That is useful conformance evidence for those cases. It is not a proof for every input, and it does not establish memory safety. Suppose a proof establishes that a source implementation refines a mathematical specification. That does not, by itself, show that emitted machine code preserves the result or that its memory addresses are independent of secret data. Suppose a binary is rebuilt byte for byte by a second machine. That establishes a reproducibility fact, not cryptographic correctness.
Orange therefore proposes to make the unit of assurance a scoped claim. A claim should name its subject, property, model, target, assumptions, evidence, and outcome. Different claims about one exported routine can have different states. A conformance claim may be satisfied while a leakage claim is unresolved. A platform may be unsupported even though a mathematical proof is valid. An external validation can be recorded without being misrepresented as a theorem checked by the Orange kernel.
The intended outcomes also need more precision than success and failure. A claim can be satisfied, not satisfied, unresolved, or unsupported. A timeout is not a proof failure, but it cannot become a proof success. An assumption is a visible dependency, not evidence that proves itself. A neighboring implementation’s test result cannot silently migrate to the implementation being shipped.
In the proposed design, this discipline would change the shape of a build. Instead of producing a binary and then attaching a broad adjective, the build would produce an artifact together with a graph of narrowly worded claims. Each edge would name the authority that justifies it. Some authorities may be machine-checked proofs. Some may be checked certificates or test runs. An owner review may support only an explicitly scoped owner-audit or governance record; it cannot impersonate a technical proof, external validation, certification, or independent review. Identified external records retain their external scope and authority. These differences would remain visible.
Trust does not disappear
Formal methods can shrink and clarify trust, but they do not make trust vanish. A small proof kernel is still software. The statement fed to it can be wrong. The parser can construct the wrong syntax tree. A compiler model can omit an instruction behavior. An assembler or linker can break the connection to final bytes. A foreign caller can violate a buffer contract. A CPU, operating system, or entropy source can behave outside the model. A release account can be compromised.
Orange’s intended response is to publish the trusted computing base for each kind of claim and to keep it specific. The trusted base for a parser behavior claim is not the same as the trusted base for a native constant-time claim. A component appears because a claim actually depends on it, not because every claim inherits one project-wide trust list.
Tests remain important inside this approach. They find regressions, exercise error paths, compare implementations, and expose resource failures. They can also provide the right basis for an empirical claim. The boundary is that a test does not change its authority when a stronger proof is missing. Honest evidence is useful evidence precisely because its limits are recorded.
What exists now
The current Orange implementation is deliberately narrow. The permanent Rust
compiler lineage provides source identities and UTF-8 byte spans, deterministic
lexing, stable diagnostic codes, and the orangec command-line boundary. The
Orange 2026 parser recognizes exactly one edition declaration followed by one
module. Legacy empty spec and impl functions remain valid. The accepted
S3a slice adds closed typed-literal specifications, the S3b slice, whose
specification is in the owner’s review, adds pure functions over integers and
machine words, the S3c slice, also in review, adds let bindings and
explicit as conversions, the S3d slice, also in review, adds fixed-length
arrays of those types, the S3e slice, also in review, adds loops over literal
ranges, indices proved in range, and updates of one element, the S3f
slice, also in review, adds Bool, comparisons, Euclidean division, and
conditionals, the S3g slice, also in review, lets an index depend on data
while still proving it in range, the S3h slice, also in review, lets a
module use other modules, each in its own file, and call their functions by
module name, the S3i slice, also in review, adds the integers modulo a
constant and names for types, the S3j slice, also in review, lets a loop’s
step and each branch of a conditional begin with let bindings, the S3k
slice, also in review, adds tuples and tuple patterns, so that a function
gives several values and a loop carries several accumulators, the S3l
slice, also in review, adds byte strings, joins, and slices, so that a
program writes bytes as the standards print them, the S3m slice, also in
review, adds size parameters, so that one function stands for every length
in a range and is checked for each, the S3n slice, also in review, adds
byte orders, so that words are read from bytes, and written back, in one
conversion in the order a standard names, the S3o slice, also in review,
adds type parameters, so that one function stands for a list of types, such
as several prime fields or both of SHA-2’s word widths, and is checked for
each, the S3p slice, also in review, lets arrays, array literals, and byte
strings hold up to 65,536 elements and lets orangec eval run under a larger
step budget, evaluate only the functions it names, and report the steps each
used, the S3q slice, also in review, adds known-answer tests and equality of
whole arrays and tuples, so that a module states what its functions must give
and orangec test checks it, and the S3r slice, also in review, lets the
amount of a shift or rotation be computed from data, with the value the
arithmetic gives at every amount.
PR #9 merged that bounded pre-alpha implementation and its normative records as
commit 6c0bd3021cf2df603e08808e4660724ca1e2b2a5. The larger S3 milestone and
the D-004 architecture decision remain open. D-003 candidate PF-01 is accepted
through OEP-0004 at exact revision
a82a5cec2ee4359dc2fe66171f17c93146747333.
edition 2026;
module demo {
spec identity() {}
impl rounds() {}
spec answer() -> Int { 42 }
spec mask() -> Word[8] { 0xff }
spec ch(x: Word[32], y: Word[32], z: Word[32]) -> Word[32] {
(x & y) ^ (~x & z)
}
spec sample() -> Word[32] { ch(0x510e_527f, 0x9b05_688c, 0x1f83_d9ab) }
}orangec check lexes, parses, and semantically validates that source. Function
names must be unique within separate spec and impl namespaces, so the two
kinds may share a spelling while a same-kind duplicate fails. Semantic type
acceptance is contextual and exact: Int denotes mathematical signed integers,
and Word[n], for n of 8, 16, 32, or 64, denotes the integers modulo 2^n. A
word literal must already fit, with no wrapping, truncation, or coercion; word
arithmetic wraps because that is what arithmetic modulo 2^n means.
Successful typed specifications lower in source order to a bounded Typed
Reference Core. Running orangec eval FILE prints:
demo::answer: Int = 42
demo::mask: Word[8] = 0xff
demo::sample: Word[32] = 0x1f85c98cEmpty declarations still have no type, value, or execution meaning, and a
function with parameters runs only when it is called. The Core is noncanonical
and carries no proof identity or relationship between a spec and an impl.
The fragment has no recursion, general failure values, proof terms, targets,
ABI rules, or code generation.
The reserved words game, proof, and claim still introduce no usable
constructs.
These absences are not disguised as a miniature finished language. The parser, semantic analyzer, Core constructor, and evaluator are bounded components at their intended incremental boundaries. Parse success means the source has the recorded syntactic shape. Semantic and evaluation success means only that a typed specification satisfied the rules and produced the displayed value. Neither result means the source is correct cryptography, a valid proof, safe machine code, a refining implementation, or a generally executable program.
This is the project’s no-disposable-prototype rule in practice. Orange grows by adding permanent components with explicit interfaces, deterministic behavior, diagnostics, tests, and migration rules. The rule does not make the early system large. It makes each small piece honest about where it belongs and what it can show.
The reader’s habit
The central habit of this book is to ask one question whenever a strong sentence appears: what connects that sentence to the exact artifact under discussion?
Sometimes the answer will be a directed project decision. Sometimes it will be a normative rule and a conformance test. Later, it may be a proof term, a checked translation certificate, an object-code inspection record, a standards source, or an external validation with exact scope. Often, during pre-alpha development, the answer will be that the connection is proposed or does not exist yet.
That last answer is not a defeat. An explicit gap is a tractable engineering fact. A hidden gap is an unbounded trust claim.
Orange’s first thesis is therefore simple: the path from intent to shipped bytes must be part of the product. Its second thesis follows immediately: every claim about that path must say what it covers, what supports it, and where it stops.