You're pledging to donate if the project hits its minimum goal and gets approved. If not, your funds will be returned.
AI safety claims are almost always binary: a system is called safe or unsafe. Rice's theorem (generalized to abstract semantics by Baldan-Ranzato-Zhang) and Pichler et al.'s no-free-lunch result on backdoor detection prove this is mathematically dishonest, since no algorithm decides non-trivial behavioral properties and no detector universally finds hidden model behavior. This project builds the alternative: a four-state output classification (PROVEN, APPROXIMATION, ESCALATED, TERMINATED), each with a distinct epistemic warrant, plus a composition calculus adapted from differential privacy so bounded-risk certificates combine soundly. An opening working paper is already public: https://doi.org/10.5281/zenodo.21341445
The goal is a complete, citable framework giving AI assurance an honest output vocabulary grounded in the impossibility results. Three phases over 9 months: Phase 1 formalizes the four-state semantics and its soundness conditions; Phase 2 develops and proves the composition calculus for homogeneous and mixed certificate sequences; Phase 3 maps the framework onto NIST AI RMF, ISO/IEC 42001, the EU AI Act, and the frontier-lab safety frameworks, then writes up the full results for open publication. Success is a formal specification with proven soundness conditions, machine-checkable composition theorems, and a published paper usable by a standards body or safety team.
Nine months of full-time research at a tax-inclusive stipend, plus compute and tooling for proof automation and SMT solver infrastructure. Total request $115,000: $90,000 stipend (tax-inclusive), $6,000 compute and tooling, $10,000 buffer, $9,000 health insurance and self-employed operating costs.
I am an independent researcher working across formal verification, cryptography, and AI governance, with a technical background in Lean 4, Z3 and cvc5 SMT solvers, and Rust. My directly relevant track record is the working paper that establishes this project's framing and novelty claim, already published with a permanent DOI: https://doi.org/10.5281/zenodo.21341445. Producing it required exactly the literature command, formal reasoning, and technical writing the full project needs. This would be early-stage funding for an independent researcher.
The main risk is that the composition calculus for mixed-grade certificate sequences proves harder to make sound than expected, in which case the framework would ship with the four-state semantics and single-grade composition, still a usable contribution, but with the general composition result left open. A softer failure is slower progress if the work is done part-time. In the worst realistic case the output is a published specification without complete machine-checked proofs, which still advances the field's vocabulary even if it falls short of the full goal.
$0. This is my first funding application for this project. A parallel application to LTFF was submitted on 2026-07-13.