Show HN: Forall – Spec-driven AI coding with formal verification

Core Premise: Specification-First, Not Prompt-First

Forall reframes AI-assisted programming: specifications—not natural-language prompts—are first-class inputs. Users write formal specs in a Coq- or Liquid Haskell–inspired syntax (e.g., forall x: int. x > 0 → f(x) % 2 == 0). The system parses these, injects logical constraints into LLM prompts, and triggers automated verification before final code acceptance.

• Spec language grounded in SMT-LIB v2, supporting quantifiers, linear integer arithmetic (LIA), and bit-vectors;
• Default backend: Z3; configurable to CVC5 or cvc5;
• Full spec parsing, constraint injection, and verification occur locally—zero external API calls.

Architecture: A Three-Stage, Verification-Augmented Generation Pipeline

Forall decomposes LLM-based code synthesis into three modular stages:

1. Spec Parsing & Constraint Injection

ANTLR4 parses specs into ASTs, compiles them into SMT formulas, and injects them into LLM prompts—not just as instructions, but as token-level constraints (via logit bias + rejection sampling).

2. LLM-Based Synthesis with Verification Feedback Loop

Uses locally hosted CodeLlama-7b-Instruct or StarCoder2-3b (user-provided weights). Generates candidate functions, then runs a lightweight verifier: auto-generates boundary-test cases and invokes Z3 to search for counterexamples. On failure, constructs minimal conflict reports and feeds them back for up to 3 rounds of re-generation.

3. Verified Artifact Output

Final output includes: (i) spec-compliant Python function; (ii) Coq proof stub (with lemmas to prove); (iii) SMT counterexample report (if any); (iv) coverage stats (≥98.2% spec condition satisfaction on benchmark suite).

Key Capabilities & Benchmarks

• Spec expressivity: Supports nested quantifiers, recursive precondition (e.g., len(lst) > 0 → head(lst) defined), purity declarations;
• Verification success rate: 89.3% of 127 hand-crafted spec–implementation pairs pass Z3 verification on first try; avg. retries = 1.4;
• Latency: 4.7s avg. end-to-end latency per function (M2 Ultra, 64GB RAM); Z3 accounts for 63%, LLM inference 28%;
• Deployment: FastAPI HTTP server (/generate endpoint), JSON-RPC spec submission, Hugging Face Transformers pipeline compatibility.

Differentiation from Existing Tooling

Forall targets the ‘trust gap’ in AI coding:

• vs. GitHub Copilot: No spec understanding—relies solely on NL prompts;
• vs. Lean Copilot / ProofGeneral: Focuses on executable Python (not theorem-proving languages), lowering barrier to entry;
• vs. Diffy / RAG-based spec tools: Zero retrieval dependence—verification logic is fully embedded, ensuring determinism and auditability;
• Not integrated with Triton/TritonServe or vLLM; positioned as lightweight serving tool for CI/CD verification gates—not high-throughput inference service.

Open Source Status & Roadmap

Hosted at GitHub (astrio-labs/forall), MIT licensed, v0.1.0 released. Next steps: (i) TypeScript/Go spec extensions; (ii) WASM-based Z3 for browser-side verification; (iii) Forall Serverless (AWS Lambda + Cloudflare Workers); (iv) arXiv tech report submission: Forall: Specification-Driven Code Generation with Embedded Verification (arXiv:2504.XXXXX).