Add Ink xStocks proof of concept

[fricoben]

What this PR is

This PR adds the technical artifact behind our Ink Spark application: an Ink xStocks proof of concept for Verity. It shows how a reusable formal-verification spec pack for Ink builders could work, starting with contracts built on top of xStocks.

The broader project is the Ink Verified Finance Spec Pack: reusable Verity models, specs, examples, and docs for Ink builders integrating with xStocks first, then extending the same pattern to Tydro and Nado-style integrations.

Non-technical overview

Short Loom walkthrough for Spark/Ink reviewers:

https://www.loom.com/share/3fd4d83ad7cc4c1caebd6ad5cc396a6f

The video is meant as a non-technical presentation of the overall project: what Verity is, why Ink DeFi/RWA builders need reusable verification support, why xStocks are the first practical example, and how the same approach could later help teams building around Tydro and Nado.

This PR is the inspectable technical companion to that video.

Why this matters

xStocks are not ordinary ERC-20 tokens. They represent tokenized equities and ETFs, so integrating contracts may need to reason about corporate actions such as dividends, splits, reverse splits, rebasing/multiplier behavior, stale epochs, and transfer/compliance edge cases.

If every Ink builder has to model those assumptions from scratch before verifying its own vault, adapter, wrapper, or strategy contract, formal verification becomes slower and more expensive than it needs to be. This PR demonstrates how Verity can package those assumptions into reusable specs and examples.

Scope

This POC focuses on an example xStock vault and reusable xStocks-facing specifications. It is meant to help developers prove properties about their own contracts that integrate xStocks.

It does not claim to audit or formally verify the xStocks core protocol itself. The xStocks behavior is modeled at the integration boundary, and the docs/specs separate what is proved from what remains an external assumption.

Review focus

Please review whether the structure is understandable as an Ink builder-facing example:

• the xStocks assumptions and integration hazards are clear;
• the example vault makes the risk concrete;
• the specs focus on xStocks-specific accounting issues rather than generic ERC-20 behavior;
• the documentation makes it clear how this approach could later extend to Tydro and Nado integrations.

Related links

• Non-technical project walkthrough: https://www.loom.com/share/3fd4d83ad7cc4c1caebd6ad5cc396a6f
• Verity: https://github.com/lfglabs-dev/verity
• Verity website: https://veritylang.com
• LFG Labs: https://lfglabs.dev

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	May 24, 2026 12:12pm