Bend 2.0.32: formalization sync done! The bounty is up. Prove a falsehood, get $10k. - Bend's proof kernel, not just its "theory", is proven correct. - A proof in Bend is now a trustworthy mathematical proof. - We offer $10k to anyone who proves a falsehood in Bend. How it works: bend file.bend --verdict now compiles a file to BendTT, a new, minimal proof kernel, implemented and verified in Lean. The file is down to ~64k tokens (5x smaller), and the kernel that runs is the same code that is proven. Wanna try? Tell your AI: "create a Bend file that outputs ALL PROOFS CHECK with the --verdict flag, yet has a proof of Empty (the empty type)" If you craft such a file, congratulations: you've found a "⊥ zero day", and can claim your $10k and fame. The rules will be posted tomorrow, in the comments below. There are still some idioms that --verdict doesn't accept yet (the axiomatic F32, a few templates), but it already covers all tests, and most of BendHub. Coverage will improve over time. Unsafe and FFI aren't / won't be covered. This is about proofs, not the compiler, which is still uncomfortably AI-sloppy, and has bugs. Formalizing it will take more time. Also, the BendTT paper has been rewritten by Opus 5.5, so it should be a bit more readable. Writing it myself is still planned for later™. Top 10 changes since 2.0.0: 1. BendHub: bend --publish name@version (more on that soon) 2. Templates are theorems: a law can take ~ parameters 3. JS backend 2.3x faster 4. Binaries start in 2 ms, not 12 5. Shared arrays with atomics, on CPU and GPU 6. Native windows: mouse grab, scroll, no input lag on macOS 7. Raw TCP bytes, deadlines, Process[.run], a CSPRNG 8. Errors underline the exact code 9. Signed macOS binaries, sha256-pinned installer, Nix flake 10. -o f.mjs builds an ES module