Verification Matrix
Click any cell to trace evidence from claim to reproducible result. Every verification method mapped to every system in the RFT-SIRM ecosystem.
Rift L1 Blockchain Core
Standalone validator core enforcing supply conservation, mint/burn accounting, dust bound, and debt limit across every state transition. O(1) distribution via global_field scalar. Checked arithmetic throughout.
Key result: 1 trillion+ operations fuzzed with zero invariant violations. Seed-reproducible. CI-integrated (5h 55m per run, ~5.75M ops/sec).
$ ./target/release/fuzz_integrated --seconds 300 --threads 4
[ 60s] cases=345M ops=1.38T ops/sec=5.75M
[ 120s] cases=690M ops=2.76T ops/sec=5.75M
[ 300s] cases=1.73B ops=6.92T ops/sec=5.75M
DONE. Total ops: 6,920,000,000,000+ Violations: 0 Crashes: 0
Evidence & Links
- Repository → Rift-L1-Blockchain
- CI Pipeline → GitHub Actions
- Invariant definitions: I1–I4 (Supply, Mint/Burn, Dust, Debt)
- Differential validation: Python reference model vs Rust impl
- 5 stratified fuzz modes: positive, negative, boundary, churn, mixed
- Limitation: No p2p / consensus layer tested
ABIv2 Memory Contexts
Research into writable permission leakage during nested CPI calls under Agave SVM ABIv2. Dynamic region count calculation with per-frame rollback.
Key result: 4.29 billion+ executions. 1 PoC-only bug documented. Upstream uses abi_v2_prepare_for_instruction architecture (svm#25 closed).
Evidence & Links
- Repository → agave-abiv2-memory-contexts
- Upstream Issue → svm#25
- Focus: Per-frame writable permission rollback
- Finding: 1 PoC-only bug (not merged)
- Limitation: Research artifact, not production patch
Agave Conflict-Aware Scheduler
Addresses unbounded deferral latency under sustained account-level write contention. Conflict-graph scheduler with bounded retry semantics and generation-based aging.
Key result: 91M executions per run, ~4,300 exec/sec. RFC published (agave#14274). Not a production patch — research artifact.
Evidence & Links
- Repository → agave-rift-scheduler
- Upstream RFC → agave#14274
- Invariants: Accounting, Monotonicity, Pass Counter, Deferred Drain
- Coverage: ~2,661 features, ~436 corpus entries
- Limitation: Not integrated into Agave validator
Aave V4 Hub Model Review
Model-level review of Aave V4 Hub invariant system. RAY = 10²⁷ fixed-point arithmetic with explicit rounding modes. Boundary matrix B-1…B-5.
Key result: 184,000 operations, 0 invariant violations. R-01 dust events (expected rounding). R-02 liquidity checks passed.
Evidence & Links
- Repository → aave-v4-hub-model-review
- Memo → MEMO.md
- Scope: draw, restore, reportDeficit, eliminateDeficit
- Precision: RAY arithmetic, explicit rounding
- Limitation: Model-level, not bytecode audit
seL4 CDT Complementary Verification
Deterministic state-machine fuzzing of seL4 Capability Derivation Tree. Complementary to the existing formal proof — not a replacement.
Key result: 1 billion+ operations, 0 kernel crashes. 123/123 post-marathon tests passed. Independent confirmation of formal proof.
Evidence & Links
- Repository → UltraCore-RFT
- Target: Capability Derivation Tree (CDT)
- Method: Deterministic replay with seed-generated ops
- Result: 0 crashes, 123/123 tests passed
- Limitation: Complementary, not replacement of formal proof
Rift Network — Solana Protocol
On-chain protocol implementing SIRM economic invariants on Solana. Independent security audit completed with 14 findings, all addressed. RC v1.0 status.
Key result: 2.5 billion+ fuzz runs. 14 audit findings fixed. All invariants enforced at contract level.
Evidence & Links
- Repository → UltraCore-RFT
- Framework: Anchor + SPL on Solana
- Audit: Independent security review, 14 findings
- Status: All findings addressed, RC v1.0
- Limitation: Audit report under NDA; summary only public
Evgeny Theorem — Gauge-Invariant Fourth Spectral Moment
Closed-form identity for the trace defect between a non-commuting SU(2) configuration and its commuting control: Δm(H⁴, θ) = −16·(3m−1 + 1)·sin²(θ/2). The normalized invariant converges to −8/9 at θ = π/2.
Key result: closed form matches direct computation at every tested (m, θ), m = 1…7 (dim(H) up to 6564). Held-out deviation ≤ 3×10⁻¹¹, gauge residual 8×10⁻¹⁵, 6/6 acceptance criteria passed.
Evidence & Links
- Repository → Evgeny-Theorem
- Live visualization → rft-sirm.github.io/Evgeny-Theorem
- Method: direct trace computation of both operators vs closed form; held-out parameters; random gauge transformation
- Result: 6/6 acceptance criteria, gauge residual 8×10⁻¹⁵
- Reproduce: pytest tests/ -m "not slow" -v
- Limitation: fourth moment only; operator-level identity not yet machine-checked (Lean file is a scaffold); not a complexity-theory result