Case file / The escrow authorization test

The buyer signed.
Should the
contract pay?

A 10 test ETH escrow. One wrong authorization check. Follow the transaction, inspect the fix, then look inside the toolchain that built it.

Follow the defect → Play the demo ↗

Daniel LiezrowiceEngineering Software Lab · MantiQ / Solidity

Amp · Solidity · Wolfram · Lean 4 · ESL SBOMator. Prepared teaching fixture, not a production escrow or a security guarantee.

The investigation / Three questions

Working code is only the first question.

ESL brings the implementation, the mathematical model, and the software inventory to the same review.

01

What does the code do?

Amp prepares the defective and corrected fixtures. Local EVM tests show exactly how they behave.

02

Do the rules hold?

Wolfram explores the model; Lean checks six model theorems. The implementation-to-model gap stays explicit.

03

What did we build it with?

ESL SBOMator identifies packages, advisories, and missing license evidence behind the build and tests.

Your contact: Daniel Liezrowice. Bring a repository, intended behavior, and existing test evidence to scope a repeatable demonstration.

ESL service context: software verification and evidence preparation. Brochure: ESL FDA Software Evidence Services, p. 9. This Solidity demo makes no medical-device or regulatory approval claim.

The business scenario · one funded supplier milestone

One deadline. Two allowed exits.

Before deadline

Buyer may release to the configured supplier.

deadline

At / after deadline

Buyer may refund. Terminal states cannot settle again.

Failed calls leave state and ledger unchanged. Recipient transfer failure must revert settlement.

Intentionally seeded fixture

Right signer.
Wrong caller.

Defective

tx.origin == buyer

An intermediary call still carries the buyer as transaction origin.

Corrected

msg.sender == buyer

The immediate caller must be the buyer.

Buyer signs→Untrusted intermediary→Escrow→Configured supplier

Precondition: the buyer signs the intermediary transaction. This is not a remote unauthenticated drain, and funds do not go to an arbitrary thief.

Exhibit A / Measured local EVM outcomes

Same interaction.
Different balance.

Defective escrow0 test ETHremaining after release

Corrected escrow10 test ETHretained; call rejected

The defective escrow pays the configured supplier. The corrected escrow rejects the intermediary.

12EVM checks

20generated sequences

108generated actions

solc 0.8.37 · optimized Shanghai bytecode · Ganache in-process EVM. Deadline boundaries, exact balances, repeated settlement, and failed-transfer rollback are checked.

Measured defective and fixed escrow outcomes from the local EVM — Real transactions and measured balances, not a simulated success animation.

Exhibit B / Wolfram model exploration

What happens at the exact deadline?

7,776 finite model cases. The boundary matters:

Buyer call at	Release	Refund
deadline − 1	Released	Funded
deadline	Funded	Refunded
deadline + 1	Funded	Refunded

Independent enumeration checks guard behavior, terminal states, and abstract conservation. Counterexample search finds the caller/origin mismatch.

Finite model exploration is not exhaustive EVM verification.

Wolfram evidence panel from the actual completed demo run — Actual exported Wolfram results, displayed by the evidence dashboard.

Exhibit C / Lean 4 kernel-checked proofs

Six theorems.
Not a blank cheque.

Unauthorized release rejection, unchanged rejected calls, terminal absorption, exclusive time windows, abstract conservation, and a concrete tx.origin counterexample.

Not proved: correspondence between the model and Solidity source or bytecode. Gas, external calls, reentrancy, and transaction ordering remain outside this model.

Lean 4.33.1 · no proof placeholders · model and assumptions included in the MIT repository.

Actual Lean build evidence listing six model theorem names and their scope — Actual theorem inventory from the completed Lean build.

Open item / Olympix access

No scan. No green tick.

Installed

VS Code extension 2.0.2 and Windows CLI 0.11.119. The CLI download checksum was verified.

BLOCKED

Account access was rejected. Daniel contacted Olympix support; no authenticated scan has completed.

Next measurement

Run the real scan, capture JSON, and check whether it identifies the seeded authorization defect.

No finding screenshot is shown because there is no completed Olympix scan. Blocked never means passed.

Official CLI documentation: https://olympix.github.io/cli/. Static analysis is documented as free; premium test generation is outside v1.

ESL's software supply-chain evidence platform

The contract is small.
Its toolchain isn't.

ESL SBOMator builds a software bill of materials: what is inside the software. SBOMator connects that inventory to known vulnerabilities, license evidence, and engineering review.

Open this demo's actual report ↗

Inventory

Generate CycloneDX component and dependency evidence, including versions, suppliers, and licenses.

Assess & explain

Correlate advisory sources; inspect dependency graphs; document vulnerability status and justifications with VEX.

Retain & monitor

Produce SBOMs, reports, and review records. Broader product workflows support rescanning, change tracking, and lifecycle evidence.

Based on ESL brochures: SBOMator CRA Compliance, Part 1, pp. 2–5; Technical Differentiators, Part 2, pp. 10–14. Product capabilities are not a claim that every feature ran in this demo. SBOMator supports evidence preparation, not certification.

The actual MantiQ-Solidity report · 20 September 2026

77 unknowns.
77 sourced answers.

368components

7unique advisories

0missing licenses

Four direct dependencies: solc, ethers, Ganache, fast-check, plus transitive development packages.

Inventory quality gate: PASSED. All 368 components now declare licenses. The 77 gaps were resolved using exact-release metadata and artifact evidence.

Explore the full HTML report ↗

License enrichment only; all 8 vulnerability records remain. 77 source citations · Original report. Declared licenses are not a legal compliance verdict. No fresh CVE scan.

License-enriched SBOMator report showing 368 components and seven advisory IDs without the missing-license warning — Real SBOMator 1.4.8 output for MantiQ-Solidity, not a product mockup. Report labels advisory IDs as “App CVEs”; these seven IDs are GHSAs.

Read the findings precisely

The findings didn't disappear.

Package	Version	Records
sha.js	2.4.11	1
serialize-javascript	6.0.0	5
bn.js	4.12.0	1
bn.js	5.2.1	1

The same advisory appears on two bn.js versions. That explains 8 records in the dashboard versus 7 unique IDs in the report.

Package matches are not proof of exploitability in this demo. Triage reachability and update options; do not suppress a finding to make the screen green.

Real SBOMator component vulnerability table with sha.js, serialize-javascript and two bn.js versions — Four affected component/version entries. These are development-toolchain dependencies, not code deployed with the Solidity contract.

From a package list to dependency context

Why is that package here?

Tab to a visible package node and press Enter to inspect its evidence and relationships. Use the component-table filter for exact package lookups.

The graph makes the build and test toolchain visible alongside the escrow code.

Open the interactive graph ↗

Dependency relationships do not establish function-level reachability or on-chain exploitability. This recorded graph limits its default view to 180 nodes; its search can select the project root. Use keyboard selection if clicking does not update the details panel.

Interactive dependency graph from the real MantiQ-Solidity SBOMator report — Actual graph embedded in this report. It is not an unrelated customer example.

The ESL evidence handover

Don't take the slide's word for it.

Provenance

Revision, dirty state, creation time, and genuine SHA-256 hashes for source files.

Honest states

Pending, running, passed, failed, blocked, and findings remain distinct.

Recorded replay is labelled as recorded. Local execution is labelled live. Missing evidence stays missing.

MIT source repository ↗ Download evidence JSON

The report adds verified license declarations to the recorded inventory. Enrichment audit · CycloneDX SBOM. The original report remains available; vulnerability findings are unchanged. Third-party products and brand marks retain their own rights; inclusion does not imply endorsement.

Presenter hand-off · run or replay

Your turn.
Open the evidence.

Play the five-stage evidence tour, pause on a finding, and open the full SBOMator report.

Launch automated demo →Open SBOMator report ↗

For live local execution:

python demo.py serve

Public GitHub Pages hosts recorded replay only. The loopback Python server enables real local checks.

Actual dashboard with passed EVM, Wolfram and Lean stages, blocked Olympix, and SBOMator findings — Click to explore. Findings and unavailable access remain visible.

Continue with ESL

Which assumption would you test first?

Discuss a scoped pilot around your software, dependencies, test suite, and verification goals.

Daniel LiezrowiceEngineering Software Lab · Israel

daniel.l@eswlab.com
+972 9 8855803
Ha-Nagar 24 A, Hod Hasharon, Israel

Contact ESL ↗

A practical first conversation

What must the software do? What evidence already exists? Which unknowns matter most?

Educational demonstration, not an audit, certification, or production-readiness verdict.

Sales: sales@eswlab.com · eswlab.com