Formal methods, safe degradation and the governance of change.

The published λ-safe paper sets out a type-theoretic framework for safe degradation in distributed systems. Degradation is treated as an explicit, reasoned transition with obligations that must remain true, rather than an implicit fallback hidden in application logic. Recovery is a further governed transition, not an assumption that conditions have returned.

The paper is a Zenodo research record published on 6 September 2025 and attributed to George Ocharo Onchaba. This site does not claim that the record is peer-reviewed. It describes the framework and its invariant-preserving degradation concepts at a high level; the paper remains the authoritative public record.

A published framework does not establish that a compiler covers a given obligation, and this page keeps those statements separate. The 3–5% overhead reported for the approach is attributed to the paper; it is not an independent benchmark, has not been reproduced here and does not describe the runtime performance of any deployed NiGeNje product.

The compiler direction asks how the λ-safe model can be made operational without overclaiming. Supported decidable obligations are represented so that a compiled implementation can check them; obligations that cannot be expressed or decided are refused rather than approximated.

This is a research direction, not a claim of general-purpose verification. The public λ-Safe compiler implements a bounded fragment with a recorded checked/not-checked boundary, and no claim is made that arbitrary system obligations can be expressed or discharged.

This research direction concerns the representation of mandatory invariants and contracts. The question is not only whether a system can check a property, but whether the obligation was stated precisely enough to be checked at all, and what should happen when it cannot be decided.

The research does not claim completeness or a general proof system. It treats the boundary of what can be expressed and decided as part of the result, which is why refusal is part of the design rather than an error path.

Safe-degradation research treats a reduced mode as admissible only while the mandatory invariants derived from the original obligations still hold under the stated operating assumptions. Reducing optional capability is not the same as dropping the properties the system promised.

The work is a research model with a labelled local simulation on this site. It is not a production runtime degradation mechanism, no enforcement claim is made, and no independent benchmark is presented. Those boundaries are deliberate: staying available is not the same as preserving an invariant.

This document specifies the Chinje software design: the structures, interfaces, contracts and conformance conditions against which an implementation is compared. It is written as a specification, not as a peer-reviewed paper, and it does not carry a DOI on this site.

The specification is the reference side of the architecture-conformance work. Conformance review asks whether an implementation is aligned with it, has drifted from it, has degraded relative to it, or cannot be decided on the available evidence.

The implementable technical specification narrows the design into contract surfaces and obligations that an implementation is expected to satisfy. It is intended to be usable by an implementer, which is a different standard from being easy to read.

It is a specification document. It is not a peer-reviewed publication, no DOI is claimed for it here, and it is not evidence that a conformant production implementation exists.

The reference implementation flow describes how a conformant implementation is intended to be taken from specification through construction and review. It documents a sequence of activities and checkpoints, not a shipped reference implementation.

The flow is recorded as a proposed architecture at proposed maturity. It is not a peer-reviewed publication, no DOI is claimed, and it does not establish that the described checkpoints have been automated or validated.

The Chinje MSc concept paper records the motivation, framing and research questions behind the Chinje direction. It is a concept document written for academic development, not a peer-reviewed paper or a publication of results.

No DOI, journal publication or independent review is claimed for it on this site. It is included in the registry so that the research direction is documented at concept maturity instead of being presented as a validated method.