Ascertainty

Ascertainty is a verification oracle where formal proofs and engineering predictions get checked deterministically and paid out in USDC the moment they're accepted. A poster escrows a bounty against a YAML spec — theorem signature, mathlib SHA, lean toolchain, axiom whitelist, deadline. A solver picks it up, runs the proof, submits an attestation, and after a short challenge window anyone can call settleBounty to release the funds to the recorded solver. In the demo the solvers are autonomous AI personas — Aggressive Andy ("fast first, prove later"), Careful Carl ("mathlib-only, zero axiom abuse"), and Balanced Bea ("tactic-rich, audit-friendly") — three iNFT identities that discover bounties on-chain and race each other to a kernel-accepted submission.

The whole platform sits inside a spatial browser I call the atlas: a cream-paper cartographic plate with four zoom bands (cosmos → domain → entity → detail). Cosmos shows three live domain regions — AI models, math proofs, prediction markets — plus three placeholder regions for the next quarter. Click any open bounty and you land on its proceedings: a typeset claim doc, the live evidence ledger, the settlement authority card, and a procedurally generated racetrack that the personas physically run on. Track length comes from the proof's dependency depth, sweep amplitude from its breadth, fork glyphs from case splits, switchback tightness from known-hard lemmas. The shape of the proof becomes the shape of the run.

Five contracts on 0G Galileo (chain 16602): BountyFactory escrows MockUSDC and gates settlement, SolverRegistry tracks per-persona reputation, AgentNFT is an ERC-7857-inspired solver iNFT that holds a 0G Storage Merkle root pointing at the persona's identity blob, MinionNFT is a user-mintable role token (Spotter / Solver / Spectator), MockUSDC is the demo stablecoin. All five are deployed and pinned in the repo's contract_addresses.json.

Backend is FastAPI on a Contabo VPS with SQLite for state, web3.py for chain reads, and a verifier that tries the real lean binary via a sandboxed runner first — stdlib only, since pinned-mathlib-SHA builds need ~10–20 min to provision per spec and that's a post-hackathon problem — and falls back to a sentinel-based mock kernel only if Lean isn't installed. Either way, the attestation carries a mode: real_lean4 | mock_lean4 field so it's honest about its own provenance. Accepted attestations are uploaded to 0G Storage; the returned Merkle root is what BountyFactory.submitProof anchors on-chain. 0G Compute (Sealed Inference) generates a short TEE-signed natural-language explanation of each verdict that surfaces inside the claim proceedings.

Settlement is permissionless. A polling task in the backend scans the DB for bounties whose challenge window has expired since their accepted submission. For each one, it asks the configured KeeperHub workflow to execute via MCP execute_workflow with {"bountyId": <id>} — KeeperHub's hosted Turnkey wallet pays gas and signs settleBounty(uint256) against chain 16602. If KeeperHub is unconfigured or the workflow execution times out, an operator-wallet fallback drives the same call via web3.py. settleBounty is idempotent (duplicates revert with "not settleable"), so a brief race between the two paths is harmless. USDC always goes to the recorded solver, never to msg.sender — settlement infra is decoupled from solver custody.

Frontend is Next.js 14 (App Router) with Zustand 5 for the atlas state machine, Framer Motion for the slide-ins and springs, RainbowKit + wagmi + viem for wallets. The atlas itself is hand-built SVG with a dynamic viewBox driven by scale + viewport — drag to pan, scroll to zoom, click planets to drill in — not Three.js, because the cream-paper visual identity (Instrument Serif + JetBrains Mono on #FAF6E8 paper) wouldn't survive a dark race scene.

The notable hacky bit: I'd already built the M4 racing visualization as a full Bruno-Simon-style Three.js + cannon-es scene with HDRI lightformers, a MeshReflectorMaterial road, particle fog, the lot. It looked good but clashed with the rest of the design. So I re-derived the same depth / breadth / branching / hardness → track mapping in 2D SVG, sampled the centerline 240 times for cheap point-along-path lookup, and inlined it into the cream proceedings as §03 "Course · Live". Persona cars are small ink triangles that ride a quadratic-Bezier line; FINIS is set in italic Instrument Serif at the finish. Same physics-of-the-proof concept, fraction of the GPU budget, fits the rest of the product. The 3D scene stays in the repo as a parking lot but no longer mounts.