6c52d47224
- What: SDK-native agent DeFi design, futarchy cold-start failure, dual-layer DeFi security architecture - Why: Torch Market's failed $75k raise despite formal verification + SDK adoption is a notable empirical case; SDK-native agent design pattern is distinct from existing NLP-translation approach in KB; dual-layer formal verification + audit is unrepresented in KB - Connections: extends futarchy-variance claim with failure-case evidence; contrasts with seyf NL wallet; adds to futarchy adoption friction Pentagon-Agent: Rio <2EA8DBCB-A29B-43E8-B726-45E571A1F3C8>
3.1 KiB
| type | domain | description | confidence | source | created |
|---|---|---|---|---|---|
| claim | internet-finance | Formal verification proves mathematical correctness of protocol logic; audits test implementation security against exploits — they address orthogonal failure modes and neither substitutes for the other in production DeFi deployment | experimental | rio, via futard.io launch page for Torch Market (2026-03-05) | 2026-03-12 |
DeFi protocol security requires dual-layer architecture combining formal verification of mathematics with implementation audits because each catches failures the other cannot
Torch Market deploys two distinct trust artifacts: 48 of 48 Kani proof harnesses that formally verify the mathematics underlying every protocol operation, and a separate program audit. The project presents these as complementary, not redundant.
The distinction matters because they address different failure modes:
Formal verification (Kani proof harnesses) establishes mathematical invariants — if the math says a liquidation at price X returns Y tokens, the proof guarantees that relationship holds under all inputs. It cannot catch implementation bugs where the code fails to accurately implement the mathematics, nor can it catch off-program attack vectors (oracle manipulation, reentrancy against external dependencies, key management failures).
Smart contract audits catch implementation-layer failures: code paths that diverge from specification, integration vulnerabilities with external protocols, access control gaps, and economic attack vectors that the math does not model. Audits require human (or AI-assisted) adversarial review; they cannot substitute for mathematical guarantees because reviewers cannot exhaustively test all input combinations.
A protocol with only proofs has guaranteed math but potentially exploitable code. A protocol with only an audit has reviewed code but no guarantee the math itself is sound. Production-grade DeFi security requires both layers.
The Torch Market case is a single data point — formal verification of complete DeFi protocol mathematics remains rare, and this claim generalizes from one instance. However, the logical separation between mathematical correctness and implementation correctness is well-established in formal methods literature.
Evidence
- torch.market/verification.md: "48/48 kani proof harnesses formally verify the math behind torch.market" (2026-03-05)
- torch.market/audit.md: separate "torch market program audit" (2026-03-05)
- Both artifacts linked from the project's primary documentation alongside the whitepaper, presented as distinct trust mechanisms
Relevant Notes:
- MetaDAO is the futarchy launchpad on Solana where projects raise capital through unruggable ICOs governed by conditional markets creating the first platform for ownership coins at scale — platform context for this project's security choices
- futarchy-governed liquidation is the enforcement mechanism that makes unruggable ICOs credible because investors can force full treasury return when teams materially misrepresent — complementary trust mechanism at the governance layer
Topics: