Anthropic researchers, collaborating with EPFL, MIT, and StarkWare, present FlashProve, an open-source zkSNARK system for provable inference of large Mixture-of-Experts (MoE) language models. The system enables a prover to commit to model weights offline (taking ~39 minutes for Llama 4 Maverick) and subsequently generate cryptographic proofs that specific outputs were produced by that committed model, without revealing the weights. Evaluated on the 400B-parameter Llama 4 Maverick (4-bit quantized, ~17B active parameters per token) using a single H100 GPU with 24 CPU cores, the prover achieves ~110 tokens/second throughput with a proof size of 18.78 MB per 1,024-token request. This represents a 70-95x overhead compared to vLLM inference on eight H100s. The verifier checks proofs in ~17 seconds on a 24-core CPU (21 seconds single-threaded) after downloading a 6.5 MB commitment. FlashProve's architecture exploits MoE sparsity by making prover work proportional to active experts, batches requests to amortize commitment opening costs, and streams weights to fit on a single 80 GB GPU with ~290 GB host memory. The underlying zkSNARK uses an IOP compiled via hash functions (post-quantum secure), incorporating code proximity tests, linear constraints, and lookup arguments. Formal verification in Lean establishes completeness, soundness, and zero-knowledge properties in the random oracle model, with an executable Lean verifier for soundness auditing and a fast C++ verifier for deployment. Artifacts released under Apache 2.0 include the prover, both verifiers, Lean proofs, a protocol specification, and an interactive theorem visualizer.