You're pledging to donate if the project hits its minimum goal and gets approved. If not, your funds will be returned.
When an AI system posts a benchmark score or an agent claims it completed a task, the supporting evidence is often difficult for an outside party to inspect as a single, cryptographically bound record. I am building receipt infrastructure to make those evaluation claims easier to audit independently.
The core is a cryptographic evidence chain: each claim ships with a sealed evidence package - sealed measurement artifacts, environment captures, independent oracle checks, SHA-256 manifests, and an on-chain hash registry anchor - so a third party can check what was measured rather than trust a summary number.
The prototype is built and evidenced, using zero-knowledge proof performance as a concrete test domain. I built and tested AVX-512 field-arithmetic kernels for the BabyBear prime field used in Plonky3-based ZK systems, and formally verified their Montgomery reduction core in Lean 4: 12 theorems, 0 sorry, 0 axioms. The surrounding formal corpus is 31 declarations with 4 remaining proof gaps (all in MachineRefinements.lean). The hash registry is deployed and verifiable on a public Ethereum testnet (Sepolia).
The evidence discipline extends to my own claims. An early benchmark of mine suggested a 9.15x speedup; a corrected, frozen 50-sample dual-run protocol measured 1.27x instead (documented/self-published; not independently replicated). I publish the unfavorable correction, the unfavorable comparisons, and the measurement protocol. Working software is available as public, Apache-2.0-licensed reviewer-access packages; additional evidence-chain and Lean proof sources are maintained in private repositories.
The pattern is designed to generalize. The same receipt format - sealed artifacts, environment captures, independent checks, on-chain anchors - could apply to AI agent evaluations, red-team results, and benchmark leaderboards.
This request funds a bounded 13-week program with named deliverable targets. Weeks 1-3 - target: resolve the 4 remaining proof gaps in MachineRefinements.lean, taking the formal corpus to 31 declarations with 0 remaining gaps, verified by corpus-wide byte recount and compile verification, shipped as a sealed evidence package. Proof work can encounter unexpected obstructions; if a gap resists closure, the gap and the attempt are published rather than hidden. Weeks 4-8 - target: extend machine-checked coverage through the number-theoretic transform stage, with differential testing and the frozen 50-sample dual-run benchmark protocol applied to each increment, unfavorable results published alongside favorable ones. Weeks 9-11: prepare and submit an opt-in verified backend PR upstream to Plonky3 (submission is in my control; upstream acceptance is the maintainers' decision and is not promised). Weeks 12-13 - target: produce one sealed, registry-anchored evaluation receipt for an AI-agent benchmark run, a package a third party can check end to end.
$43,000 total: $32,500 research time (13 weeks at $2,500/week, full-time focus) plus about $10,500 non-time costs - dedicated AVX-512 benchmark hardware, cloud and registry operations, and contingency. $43,000 is not a valuation of the project; it is the costed scope of a 13-week research program. Each milestone ships with its evidence package: sealed artifacts, environment captures, independent oracle checks, SHA-256 manifests, and an on-chain anchor.
Solo researcher, pre-revenue, previously built all of this part-time alongside contract work. Track record is evidenced rather than asserted: a 12-theorem machine-checked Montgomery reduction core in Lean 4 (compile-verified, 0 axioms, 0 sorry), a 31-declaration formal corpus, a frozen 50-sample dual-run benchmark methodology, an on-chain hash registry verifiable on Sepolia, and a documented public self-correction of my own benchmark claim (9.15x down to a measured 1.27x under the corrected protocol; documented/self-published, not independently replicated).
Formal verification is the main risk: the weeks 1-3 and 4-8 targets are proof work, and proof work can hit unexpected obstructions. If a gap resists closure, the failure mode is honest and visible - the gap and the attempt are published rather than hidden, so the fund gets a true record either way. The upstream Plonky3 PR may be rejected or stalled by maintainers; that is outside my control and only the submission is promised. The AI-eval receipt pilot is deliberately scoped to one concrete sealed package, so a failed pilot would still document what the evidence chain can and cannot bind. None of these failure modes would silently convert an unsuccessful attempt into a success claim.
$0.00 raised in the last 12 months. No grants or investments. The work so far has been self-funded from contract work, built part-time.