Cyrup

Cyrup is a decentralized marketplace that connects people who need mathematical proofs with expert theorem provers. The platform bridges the gap between theoretical computer science and practical verification needs by creating an economic incentive layer for formal verification.

At its core, Cyrup allows users to post mathematical or logical challenges that require formal proofs, set USDC rewards, and have experts submit solutions using the Lean 4 theorem prover. The platform features a sophisticated reputation system that tracks user performance and ensures only qualified verifiers (top 10% by reputation) can validate submissions.

The system operates through smart contracts deployed on Base Sepolia, ensuring transparent and automatic reward distribution. When a proof is submitted, it goes through both automated verification via a Lean 4 runner service and human verification by qualified experts. Once both the challenge creator and assigned verifier approve a solution, rewards are automatically distributed - 95% to the solver and 5% to the verifier.

Key features include an integrated web-based Lean IDE for writing proofs directly in the browser, a comprehensive leaderboard system, gas-optimized smart contracts using clone patterns and packed storage, and a persistent Lean verification service that validates proofs in real-time.

Smart Contracts (Solidity/Foundry):

• Built with ultra-optimized Solidity contracts using packed structs, custom errors, and the clone pattern for gas efficiency
• ChallengeFactory deploys minimal proxy clones using CREATE2 for deterministic addresses
• ChallengeEscrow manages the lifecycle: challenge creation → verifier selection → solution submission → dual approval → automatic reward distribution
• ReputationSystem implements dynamic top 10% tracking with efficient threshold algorithms and tiered point calculation based on USDC amounts
• Deployed on Base Sepolia for low-cost transactions

Backend (Go/Gin):

• Microservices architecture with two separate services: API server and Lean runner
• API server built with Gin framework handles HTTP requests, database operations (PostgreSQL via sqlx), and queues verification requests
• Lean runner service runs in a Docker container with persistent Lean 4 environment, avoiding restart overhead between verifications
• Services communicate via HTTP, deployable on Railway with automatic port detection and internal networking
• Implements submission tracking with unique UIDs linking blockchain transactions to off-chain Lean code

Frontend (Next.js/React):

• Next.js 14 app with TypeScript, Tailwind CSS for styling, and wagmi/viem for Web3 integration
• Coinbase CDP SDK integration for streamlined wallet connections and transaction signing
• Monaco Editor integration provides a full-featured IDE for writing Lean proofs in the browser
• React Markdown with syntax highlighting for rendering challenge descriptions
• Custom hooks abstract contract interactions and API calls

Lean 4 Integration:

• Docker containerized Lean 4 environment with pre-built mathlib for fast verification
• HTTP service wrapper around Lean that accepts code, verifies proofs, and returns results
• Persistent container architecture eliminates cold start delays
• Database stores proof code with IPFS hashes for permanent storage

Notable Technical Achievements:

• Gas optimization through clone pattern saves ~90% deployment costs per challenge
• Packed storage reduces state variables from 8+ slots to 3-4 slots per struct
• Bitmap approval system tracks dual signatures in single uint8
• Dynamic reputation threshold algorithm efficiently maintains top 10% without full sorting
• Microservices architecture allows independent scaling of verification workload
• Integration of formal verification (Lean 4) with blockchain creates trustless proof marketplace