Proof-Driven Software Delivery with Allium and Bend

NORMAN KHINE · PUBLIC EDITION · 19 OCTOBER 2026

Connect intent, implementation and evidence.

A passing test or proof in one repository cannot explain the behaviour of an entire distributed system. This paper describes how behavioural specifications, bounded proofs, repeatable tests and retained evidence can support one reviewable delivery decision.

Allium expresses approved intent. Bend checks mathematical obligations for a formal core. Protocol-aware testing explores implementation behaviour, while immutable manifests connect the results to the software being delivered.

Read the full paper Open PDF

22 sections · 9 diagrams · mathematical notation, worked examples and references. The HTML reader supports mobile screens and browser search.

What you’ll take away

A way to distinguish proven, tested, assumed and observed behaviour.
A delivery process that binds approvals, proof obligations and test results to exact candidates.
A method for tracing the impact of changes across component boundaries.
Patterns for replay, failure evidence, recovery and UI state ownership.

Start with a question

What does “verified” mean?Separate model proof, implementation conformance, protocol testing and operational observation.From intent to proof obligationsMake the supported language fragment, assumptions and implementation connection explicit.What needs to be checked again?Follow behavioural dependencies and bind the evidence to the exact changed system.UI correctness is part of the contractExplore ordering, identity and ownership in HTMX, Elm and Datastar interfaces.Recoverability and evidence qualityUse explicit obligations and recovery checks without treating a score as a correctness probability.Scope and limitationsUnderstand which claims need further proof, implementation evidence or operational validation.

How to read the examples

The architecture applies to multi-repository software systems. Financial workflows provide concrete examples of conservation, identity, retries and recovery; they are illustrative rather than customer data. The paper separates its small checked arithmetic model from proposed system-wide capabilities and future evaluation work.

This is a generic public edition. It retains the author’s technical argument and public citations, while excluding private operational evidence. It does not claim complete verification of Abakuc or any deployed platform.

Download PDF Explore Vinculum’s interactive workflow