An ESL engineering demonstration

One escrow.
Two outcomes.
Show the evidence.

Amp-assisted Solidity development, Wolfram checks, Lean 4 model proofs, and ESL SBOMator supply-chain evidence.

Daniel LiezrowiceEngineering Software Lab · MantiQ / Solidity

Actual local dashboard: defective escrow Released, fixed escrow Funded; Olympix blocked and SBOMator findings visible — Actual demo run, 20 September 2026. No wallet, public RPC, or real funds. Select the screenshot to open the evidence tour.

Prepared teaching fixture, not a production escrow or a security guarantee.

Engineering Software Lab · Israel

ESL connects the tools to the engineering question.

This demo combines executable behavior, independent models, and dependency evidence in one reproducible workflow.

01

Build & exercise

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

02

Challenge assumptions

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

03

Expose the toolchain

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

The buyer controls settlement, not the intermediary.

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

The authentication defect

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.

Local EVM

Same signed interaction. Ten test ETH stay or leave.

Defective: releases 10 test ETH to the configured supplier.

Corrected: rejects the intermediary; all 10 test ETH remain in escrow.

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.

Wolfram

7,776 model cases. Test the exact deadline.

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.

Lean

Six kernel-checked theorems. A clearly bounded claim.

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.

Olympix

Installed, but not yet authenticated.

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

What is ESL SBOMator?

A software bill of materials answers 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 license gaps resolved with evidence.

368components

7unique advisories

0missing licenses

All four direct dependencies found: solc, ethers, Ganache, and fast-check. Transitive development packages are included.

Inventory quality gate: PASSED. All 368 components now have declared licenses. Exact-release metadata and artifact evidence resolved the offline gaps; no warning was hidden.

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

Seven advisories, eight component-level records.

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

Explore the actual software dependency graph.

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

Open artifacts, bounded claims, reproducible checks.

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

Let the audience inspect 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

Bring the engineering question.
Build the evidence with us.

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