Type-theoretic framework
The paper sets out a type-theoretic framework for safe degradation in distributed systems: a system should degrade along expressible, checked paths rather than failing into an unconstrained state.
Research and evidence
A framework is a hypothesis until the implementation is checked.
λ-Safe research explores a type-theoretic framework for safe degradation in distributed systems, with a Rust-targeting prototype and soundness proof sketches. This page separates what the paper reports from what NiGeNje has actually implemented and verified.
Research context
What the λ-Safe paper is about.
Distributed systems fail in partial, overlapping ways. When a component cannot continue safely, it usually degrades: it retries, falls back, drops work or narrows its behaviour. That degradation is often implicit, undocumented and unchecked — the moment when a safety property is most likely to be lost.
λ-Safe research proposes a type-theoretic framework for safe degradation in distributed systems. The objective is to make degradation an explicit, reasoned transition with obligations that remain true, rather than an unconstrained fallback buried in application code. The published record describes a Rust-targeting prototype and soundness proof sketches for the framework.
The research is the basis for the λ-Safe product direction, not a substitute for product evidence. A published framework does not establish that a shipped compiler covers a given obligation, and this site keeps those two statements separate.
What the paper reports
Contributions, described without inflation.
These are the paper’s stated contributions. “Reports” and “sketches” are deliberate words: they are not claims of independent validation or mechanised proof.
Safe degradation
The research frames degradation as an explicit, reasoned transition with obligations that must remain true, instead of an implicit fallback hidden inside application logic.
Rust-targeting prototype
A prototype targets Rust so that supported safety obligations can be represented in a form that a compiled implementation can check, rather than remaining prose in a design document.
Soundness proof sketches
The paper presents soundness proof sketches for its framework. Sketches are not a mechanised proof or an independent verification result, and they are described here as the paper presents them.
Reported 3–5% overhead
The paper reports 3–5% overhead for its approach. That figure is the authors' reported result, attributed to the paper; NiGeNje has not independently reproduced it and does not present it as a benchmark.
Evidence discipline
A reported result, a proof sketch and a verified implementation are three different things. This site does not upgrade one into another. Where the paper reports a figure, the figure is attributed to the paper; where NiGeNje has not reproduced it, the site says so.
Research to product
How λ-Safe research maps to the λ-Safe product.
The mapping is narrow and explicit. Research concepts become compiler and verification artifacts with a recorded checked/not-checked boundary; they do not become a general assurance claim.
Compile supported invariants
λ-Safe Core is the open-source Rust compiler that turns supported, decidable hard invariants into a manifest and a λ-certificate. The research framework is the design basis; the compiler is the implementation boundary.
Record the checked boundary
A certificate states what was checked and what was not. Unsupported or indeterminate mandatory obligations are refused rather than approximated, which is the product expression of the research position that unknown is not proof.
Carry artefacts into admission
λ-Safe Enterprise signs bundles and verifies them against a trust store; Gatekeeper consumes the resulting bundle verification at admission. Research concepts become runtime artifacts at this point.
Keep the evidence inspectable
Compilation, admission and execution records remain separate and linked rather than collapsed into an opaque success flag, so a reviewer can trace what was checked and what was assumed.
Verified destinations
Read the sources, not the summary.
The research record and the λ-Safe Core repository are public. Platform repositories are private and are not linked. External destinations are provided for direct inspection.
Collaboration
Evaluate the research against a real obligation.
Research collaboration and evaluation are discussed through the contact route. Questions about coverage start with the obligation you need represented, not with a general claim of safety.