{"author":"Nolan_Lwin","children":[],"created_at":"2026-07-16T02:16:18.000Z","created_at_i":1784168178,"id":48929654,"options":[],"parent_id":null,"points":6,"story_id":48929654,"text":"We've been working on an open-source coding agent that generates code alongside machine-checkable proofs. We'd love feedback from the HN community, especially from people interested in formal verification, Lean, Dafny, or AI coding agents. Currently, only 3 langauges can be verified.","title":"Show HN: Forall \u2013 An AI coding agent that generates machine-checkable proofs","type":"story","url":"https://github.com/astrio-labs/forall"}