Engineering note
Unknown is not proof: why λ-Safe refuses instead of guessing
A verifier that treats an undecidable clause as a pass is worse than no verifier at all. How λ-Safe records the boundary of what it actually established.
Formal tooling has a failure mode that looks like success: the analysis cannot decide a clause, so it quietly skips it and reports a positive result. The reader sees "verified" and never learns which part of the contract was never checked.
λ-Safe is built around the opposite behaviour. Supported hard invariants are checked and recorded in a scoped assurance record. A compulsory clause that cannot be expressed or decided is refused, with no positive artifact emitted and an explicit BLOCKED outcome. The record also carries a checked/not-checked boundary, so a downstream verifier can see what the analysis established rather than inferring it.
What the current implementation actually supports
The reviewed implementation supports a deliberately bounded class of static invariants. That is a fragment of the obligations a real system might want to express. It is useful precisely because the boundary is explicit: the platform can say "this obligation was checked" without implying "this system is safe".
The public λ-Safe repository makes that bounded scope inspectable. No claim is made here about unpublished extensions, and nothing on this page is a substitute for the public record.
Why the refusal path is the product
A contrast helps. If a billing system asks to "never allow a negative balance", a compiler that can express the bound should prove the bound, and a compiler that cannot express it should refuse. A permissive fallback would let the system keep the appearance of safety while removing the guarantee.
That is also why the audit record matters. The output is not a green tick. It is a bounded claim with an explicit not-checked list, which a reviewer can put next to the contract and question.
Where this stops
- The reviewed compiler covers a bounded class of hard invariants; it is not a general proof system.
- A runtime violation inside a successfully checked contract is not exercised end to end.
- λ-Safe verifies; it does not intercept or enforce actions at runtime.
- No independent benchmark, reproducible-build proof or production qualification is claimed.