StrictDoc vs. Bend 2 and Gherkin: The Tripartite Verification Stack for High-Assurance Systems

How requirements traceability, behavioral specifications, and interaction-combinator formal proofs unite to eliminate both specification gaps and runtime defects.

Executive Summary

When engineering teams first encounter Bend 2 and its integrated Lean 4 formal reduction kernel (bend --verdict), a recurring question arises:

“If our code is mathematically proven to satisfy its specification twin via interaction net reduction, does formal code render requirements management tools like StrictDoc or behavioral frameworks like Gherkin obsolete?”

The short answer is no. In high-assurance software engineering, conflating requirements management with formal verification is a category error that leads to catastrophic failures.

To build trustworthy software, an engineering organization must answer two fundamentally distinct questions formulated by Barry Boehm:

1. Validation: “Are we building the right system?” (Conformance to human intent, legal statutes, safety regulations, and domain boundaries).
2. Verification: “Are we building the system right?” (Mathematical proof that the executing implementation conforms strictly to its formal specification).

Bend 2 answers Verification with unprecedented mathematical rigor and automatic GPU parallelization. However, Bend 2 cannot validate whether the theorem you proved matches human intent, customer contracts, or safety standards.

This article presents the Tripartite Verification Stack: how StrictDoc (normative requirements traceability), Gherkin (observable acceptance scenarios), and Bend 2 (massively parallel execution with Lean 4 proof receipts) form a continuous, closed-loop assurance pipeline.

1. The Assurance Triad: Validation vs. Verification

High-assurance engineering disciplines (aerospace DO-178C, automotive ISO 26262, and medical IEC 62304) divide system correctness into three complementary layers:

flowchart TD
    subgraph Layer1 ["Layer 1: Normative Requirements & Governance"]
        SD["StrictDoc (.sdoc)<br/>Auditable UIDs, Statutory Limits, Traceability Matrix"]
    end

    subgraph Layer2 ["Layer 2: Observable Acceptance & Scenarios"]
        GK["Gherkin Scenarios (.feature)<br/>Given-When-Then Integration & Negative Paths"]
    end

    subgraph Layer3 ["Layer 3: Formal Execution & Proof Receipts"]
        B2["Bend 2 Kernel (LAWS.bend / PROOF.bend)<br/>Confluent Parallel Execution & Lean 4 Reduction Proofs"]
    end

    SD -->|"Refines into executable tests"| GK
    SD -->|"Defines mathematical invariant contracts"| B2
    GK -->|"Validates user-visible system behavior"| Runtime["Production System Runtime"]
    B2 -->|"Supplies leaf-level machine-checked proof receipts"| SD

The Three Tiers Defined

2. Why Formal Code Does Not Obsolete Requirements

A common misconception in the formal methods community is that executable code containing embedded assertions or types can substitute for a dedicated requirements management system. This fails for three foundational reasons:

1. Code Cannot Prove Its Own Intent

Consider an exchange function in an algorithmic trading engine. In Bend 2, we can formally prove:

for all units in Nat: execute_exchange(state, 4, 1, units) == Success(state_next)

The Lean 4 kernel mechanically confirms that the state transition evaluates to the exact mathematical product. However, the code cannot answer: - Why is the ratio 4:1 instead of 3:1 or 2:1? - Which financial regulation or customer contract mandates this ratio? - Who authorized the parameter change in commit 0d01c9c? - What legal statute governs liability if a transaction fails?

Code represents the mechanism. Requirements capture the intent, rationale, and authority. Without StrictDoc, the rationale is lost to git commit archaeology.

2. The Verification-Validation Gap

A program can achieve 100 % formal verification against its specification yet remain completely wrong for the business:

Code -> Formal Spec (Verification) vs. Formal Spec -> Human Reality (Validation)

If the formal specification states that integer multiplication wraps modulo 2³², Bend 2 will happily prove that 4 × 2³⁰ ≡ 0 (mod  2³²). The code is verified. But in the real world, an initiator paying 0 cost to receive 2³⁰ units bankrupts the protocol.

StrictDoc bridges this gap by enforcing explicit negative requirements (NEGATIVE_STATEMENT) that mandate checked arithmetic and rejection of integer overflow.

3. Regulatory and Audit Compliance

Auditors evaluating medical devices, avionics, or banking infrastructure do not inspect 50,000 lines of functional source code. They demand a Traceability Matrix: - Every statutory requirement must have a permanent UID. - Every UID must link to an author, rationale, verification method, and proof receipt. - A single schema change must report exactly which downstream components are impacted.

StrictDoc maintains this matrix in git-tracked, diffable text files, compiling human-readable HTML and machine-readable JSON for automated pre-push CI gates.

3. Comparison Across High-Assurance Frameworks

To contextualize where StrictDoc, Gherkin, and Bend 2 sit in the software engineering landscape, let us compare them against established industrial and formal modeling frameworks:

Key Takeaways from the Matrix

1. TLA+ and Alloy excel at finding architectural deadlocks and concurrency bugs in abstract models before code is written, but they do not generate production binaries.
2. Pure Lean 4 is the gold standard for pure mathematical proofs, but authoring proofs requires specialized mathematical expertise, and parallelizing execution across thousands of GPU cores requires complex custom runtimes.
3. Bend 2 uniquely unifies execution with verification: it compiles Python-syntax affine code to high-throughput CUDA and Metal shaders while checking computational equalities via Lean 4.
4. StrictDoc provides the overarching governance envelope that none of the formal tools provide natively.

4. The Closed-Loop Pipeline in Practice

Let us examine how a real-world security requirement flows through the Tripartite Verification Stack in the bend2-packages repository.

Step 1: Normative Requirement in StrictDoc (requirements.sdoc)

We define the requirement with an explicit negative statement, formal proof links, and GPU execution parameters in StrictDoc:

[REQUIREMENT]
UID: B2PKG-PARETO-005
TITLE: Arithmetic Overflow Rejection (Checked Multiplication and Addition)
STATEMENT: >>>
The exchange kernel shall check multiplication (units * cost_factor, units * payout_factor) 
and addition (pool accumulation) for 32-bit integer overflow before execution.
<<<
NEGATIVE_STATEMENT: >>>
An exchange causing integer wrap modulo 2^32 (such as 4 * 2^30 = 0) shall never succeed 
or grant free units. All overflow conditions must fail closed with ExchangeArithmeticOverflow.
<<<
FORMAL_SPEC: packages/pareto-oracle/LAWS.bend:law exchange_overflow_cost_multiplication_rejected
PROOF_RECEIPT: packages/pareto-oracle/PROOF.bend:def LAWS.exchange_overflow_cost_multiplication_rejected
PROOF_KERNEL: lean4_reduction_kernel
GPU_DISPATCH: supported
PARALLEL_SHAPE: tree_reduction
STATUS: implemented
SOURCE_FILES: packages/pareto-oracle/main.bend
VERIFIED_BY_TESTS: packages/pareto-oracle/tests/test_oracle.bend:test_9

Step 2: Formal Invariant in Bend 2 (LAWS.bend)

In packages/pareto-oracle/LAWS.bend, the requirement is translated into checked affine arithmetic and an explicit formal law:

# Checked multiplication preventing modulo 2^32 wrap
def mul_overflows_helper(is_zero: Bool, +a: U32, +b: U32) -> Bool:
  match is_zero:
    case True{}: False{}
    case False{}: U32.is_gt(b, (4294967295 / a : U32))

def mul_overflows(+a: U32, +b: U32) -> Bool:
  mul_overflows_helper(U32.is_eq(a, 0), a, b)

# LAW 9: Cost multiplication overflow rejected (P0 countermeasure: 4 * 2^30 != 0).
law exchange_overflow_cost_multiplication_rejected:
  {execute_ratio_exchange(State{0, 0, 0, 1073741824}, RatioFourToOne{}, 1073741824) == ExchangeArithmeticOverflow{} : ExchangeResult}

Step 3: Mechanical Proof in Bend 2 (PROOF.bend)

In packages/pareto-oracle/PROOF.bend, the proof receipt is declared via computational reduction ({==}):

import Base
import ./LAWS.bend as LAWS

# Proof of Law 9: exchange_overflow_cost_multiplication_rejected
def LAWS.exchange_overflow_cost_multiplication_rejected():
  {==}

Step 4: Verification via Lean 4 Proof Kernel

During CI and pre-push, make test invokes the Lean 4 reduction kernel:

bend packages/pareto-oracle/PROOF.bend --verdict

Output:

ALL PROOFS CHECK

The proof engine reduces both the left-hand side and right-hand side to their normal forms in interaction net geometry and confirms identity. If an arithmetic bug or integer overflow were present, Lean 4 would halt with a counterexample, and the CI gate would immediately fail closed.

Step 5: Observable Acceptance in Gherkin

At the system integration boundary, a Gherkin scenario verifies observable behavior across consumer services:

Scenario: Initiator attempts extreme volume transaction causing arithmetic overflow
  Given an initiator with 0 units of currency
  And a liquidity counterparty with 1,073,741,824 payout units
  When the initiator requests a 4:1 ratio exchange for 1,073,741,824 units
  Then the transaction must be rejected with "ExchangeArithmeticOverflow"
  And the initiator balance must remain 0
  And the counterparty balance must remain 1,073,741,824

5. Architectural Standards for High-Assurance Packages

When applying this stack to shared libraries and microservices, enforce the following five non-negotiable rules:

1. Every Law Carries a Persistent StrictDoc UID: Formal laws in LAWS.bend must cite their governing requirement UID in code comments.
2. Every Positive Requirement Demands a Negative Requirement: Never write a requirement that only describes happy-path success. State explicitly what failure condition must be rejected to prevent permissive validator bypasses and kill mutants.
3. Mandatory Kernel Verification (--verdict): Running --check-only validates types, but only --verdict executes the Lean 4 proof reduction. CI must mandate --verdict.
4. Architect for GPU-First Parallelism (2^N Tree Reductions): Structure compute kernels as binary fork-join trees so interaction net reduction scales linearly across thousands of GPU cores.
5. Enforce True Library Boundaries (LIB-001..008): Shared packages must remain completely domain-neutral, with zero leakage of consumer business concepts or internal network topologies.

Conclusion

Bend 2 and Lean 4 represent a quantum leap in program correctness, delivering provably correct code running on massively parallel GPU hardware. But formal proofs alone cannot prevent teams from building the wrong system.

Combining StrictDoc, Gherkin, and Bend 2 builds an unbroken assurance chain from regulatory statutes down to GPU shader reductions.

Published on bend2.org. Benchmarks and formal packages available in the ShipItFullSend ecosystem.