GWAYA: Fail-Closed Gate & Real Toolchain Verification for LLM Code Generation

GWAYA (Gwen-Laya Open Model) is a zero-trust, fail-closed verification layer that sits between code-generating language models (such as the Qwen / Gwen series) and execution environments.

Unlike traditional code checkers that yield false positives when toolchains are missing or models emit placeholder stubs, GWAYA is strictly fail-closed: a candidate is accepted only if real, deterministic compilers and sandboxed execution positively succeed. Every situation where checking cannot run (missing compiler, offline fallback, lack of generator) yields UNVERIFIED with maximum penalty energy ($E = 10^6$).

📌 Links to Official Releases & Reports

• Zenodo Permanent Archival (v3.1.1): https://doi.org/10.5281/zenodo.23123923

• Hugging Face Verified Artifacts & Raw Telemetry: callensxavier/gwaya-v3-verified-report

• Verified Research Report (PDF): papers/gwaya_v3_verified_report.pdf (7-page comprehensive audited report)

• Pre-Registration & Audit Trail: results/PREREGISTRATION.md

Related MCP server: Sensory-Grounding MCP

🔍 Verified Findings vs. Unverified Research Directions

In compliance with zero-trust empirical principles, this repository strictly separates mathematically & experimentally verified claims from ongoing, unverified research directions.

========================================================================================
                          GWAYA VERIFICATION LANDSCAPE
========================================================================================
  [VERIFIED CLAIMS]                                 [ACTIVE RESEARCH ROADMAP]
  -----------------                                 -------------------------
  ✓ AST Zero-Stub Audit (rejection of               ? Full Qwen Series Scaling
    pass, ..., mock_*, fake_*, sorry, etc.)           (0.5B, 1.5B, 3B, 7B, 14B, 32B)
  ✓ Fail-Closed Python Sandbox                      ? Multi-turn Execution Trace Repair
    (Bubblewrap isolation, time/memory bounds)        with Rich Exception Feedback
  ✓ Real Rustc Type & Borrow Checking               ? Lean 4 Mathlib Formal Proof
    (metadata emission, placeholder rejection)        Search at Scale (>10k theorems)
  ✓ Lean 4 Kernel Soundness Verification            ? Exemplar Retrieval Optimization
    (with #print axioms closure audit)                (Resolving A4 vs A3 degradation)
  ✓ Low-Tier Sample-and-Repair Loop                 ? Direct Preference Optimization (DPO)
    (+7.78 pt pass@1 on Qwen2.5-Coder:1.5B)           on Deterministic Fail-Closed Pairs
========================================================================================

1. Retraction of Earlier Unverified Claims

The first revision of this report (version 3.1.0, Zenodo DOI 10.5281/zenodo.23121788) included claims that the low-tier optimizer improved pass rates by at least +8.0 percentage points based on a hand-written results file. That claim was retracted. Version 3.1.1 and this open-source release report only the real, measured benchmarks described below.

📊 Measured Empirical Benchmarks (MBPP-Sanitized)

All benchmarks evaluate qwen2.5-coder:1.5b on the MBPP-sanitized test split.

• Setup: Public test is test_list[0]; hidden tests are test_list[1:].

• Outcome criterion: A problem is solved only if the final candidate passes all asserts inside an isolated Linux Bubblewrap (bwrap) sandbox. The optimizer's internal flags are never taken as proof.

• Arms:

  • A0: Raw first sample (zero-shot baseline).

  • A2: Best-of-3 candidate sampling scored against the public test.

  • A3: Best-of-3 plus up to 3 iterative self-repair rounds on public test failures.

  • A4: A3 plus one retrieved exemplar from MBPP train/validation splits (leakage-guarded).

• Pre-registered Gate: $A3 - A0 \ge +8.0$ percentage points.

Benchmark Results Table

Key Benchmark Takeaways

1. Statistically Clear Gain on Full Scale ($n=257$): In the full replication, A3 gained 20 problems and lost 0 compared to raw baseline A0 (exact McNemar $p < 0.001$), demonstrating that test-driven self-repair reliably recovers broken solutions.

2. Honest Gate Reporting: The pre-registered gate required $\Delta \ge +8.0$ points. The measured gain was +7.78 points (0.22 points below threshold). In strict accordance with the measured-improvement contract, the gate verdict is reported as FAIL without adjusting the threshold post-hoc.

3. Exemplar Retrieval Underperformed A3: Arm A4 (adding in-context retrieved exemplars) yielded +7.00 points but lost 5 previously-solved problems. Indiscriminate exemplar injection can bias small models away from straightforward solutions.

🛠️ Architecture: The GWAYA Fail-Closed Gate

For any candidate $c$ in language $\ell \in {\text{python}, \text{rust}, \text{lean4}}$, the gate accepts if and only if:

$$\mathrm{accept}(c) = \mathrm{Avail}\ell \wedge \mathrm{StubAudit}\ell(c) \wedge \mathrm{Oracle}\ell(c) \wedge \bigl(\ell \neq \text{lean} \vee \mathrm{Ax}(c) \subseteq A{\text{std}}\bigr)$$

where:

1. $\mathrm{Avail}_\ell$ (Toolchain Availability): Confirms compiler binaries are present on the host. Missing compilers immediately yield UNVERIFIED (never pass).

2. $\mathrm{StubAudit}_\ell(c)$ (AST Zero-Stub Law): Analyzes the AST to reject pass, ..., mock_*, fake_*, dummy_*, sorry, admit, unimplemented!().

3. $\mathrm{Oracle}_\ell(c)$ (Compiler/Execution Oracles):

   • Python: Syntactic non-triviality check + isolated Linux Bubblewrap execution with memory bounds, temporary directory sandbox, and strict timeout.

   • Rust: Verifies syntax, types, borrow checker, and lifetime rules via rustc --emit=metadata.

   • Lean 4: Kernel check ensuring no non-standard axioms were introduced.

4. $\mathrm{Ax}(c) \subseteq A_{\text{std}}$ (Axiom Soundness): The Lean 4 oracle executes #print axioms on every named declaration. It strictly limits dependencies to standard Lean axioms: $A_{\text{std}} = {\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}}$. Bypasses such as axiom bad : False or sorryAx are caught and rejected even if lean exits 0.

🤖 Model Context Protocol (MCP) Server for AI Agents

GWAYA includes a production-ready Model Context Protocol (FastMCP) server, enabling autonomous AI coding agents (Claude Code, Antigravity, Cursor, Windsurf, OpenHands) to inspect, verify, and repair code before executing or presenting it.

MCP Tools Provided

Connecting to Claude Code (.mcp.json)

Add the following to your project's .mcp.json or claude.json:

{
  "mcpServers": {
    "gwaya": {
      "command": "python",
      "args": ["/path/to/GWAYA-GwenLayaOpenModel/mcp_server.py"],
      "env": {
        "PYTHONPATH": "/path/to/GWAYA-GwenLayaOpenModel"
      }
    }
  }
}

Connecting to Antigravity CLI / IDE

Add to your .antigravity/mcp_servers.json:

{
  "gwaya-verification": {
    "command": "python",
    "args": ["-m", "mcp_server"],
    "cwd": "/path/to/GWAYA-GwenLayaOpenModel"
  }
}

⚡ Deployment: Consumer RTX GPUs & Ollama

GWAYA is optimized to run locally on consumer NVIDIA GeForce RTX graphics cards using Ollama.

1. Hardware VRAM Sizing Guide

2. One-Click Setup Script

We provide an automated setup script that detects your RTX card, checks VRAM, pulls the optimal model, and validates 100% GPU layer offloading:

# Clone the repository
git clone https://github.com/xaviercallens/GWAYA-GwenLayaOpenModel.git
cd GWAYA-GwenLayaOpenModel

# Auto-detect GPU and pull optimal model:
./scripts/deploy_rtx_ollama.sh

# Or pull a specific model:
./scripts/deploy_rtx_ollama.sh 7b

3. Running the FastMCP Server

uv pip install -e .
fastmcp run mcp_server.py

4. Running the MBPP Benchmark Locally

# Run 10 problems on your local RTX GPU
python scripts/run_benchmark.py --n 10 --model qwen2.5-coder:1.5b

# Run full MBPP replication (n=257)
python scripts/run_benchmark.py --n 257 --model qwen2.5-coder:7b --out-dir results/my_rtx4090_run

⚡ Local Agent Deployment: gwaya-agent CLI & Docker Compose

For developer workstations with NVIDIA RTX GPUs (RTX 3060, 3080, 4060, 4080, 4090) or CPU fallback:

1. Zero-Config GPU Doctor & CLI

# Check GPU VRAM, detect installed models, and get automated model recommendations:
gwaya-agent doctor

# Run fail-closed verified generation:
gwaya-agent ask "def is_prime(n): check if n is prime" --test "assert is_prime(7) and not is_prime(8)"

2. Full Local Stack with Docker Compose

Run both the Ollama GPU backend and GWAYA verification agent with a single command:

# Launch Ollama with GPU pass-through + GWAYA agent:
docker compose up -d

# Verify agent status
docker compose run gwaya-agent doctor

3. Anti-Hallucination Grounding & Consensus Self-Testing

Small models frequently suffer from:

• Symbol hallucinations: Inventing functions (numpyx.fast_solve), non-existent stdlib attributes, or unbound variables.

• Over-fitting to a single public test: Emitting hardcoded checks that fail hidden edge cases.

GWAYA resolves this through:

1. gwaya.grounding: Static AST and pyflakes inspection rejects candidates referencing unresolvable imports or unbound local names before execution.

2. gwaya.consensus_agent: Generates candidate unit tests from multiple independent generations and computes consensus ($k \ge 2$) assert agreement, rejecting candidates that fail consensus tests even if they pass the public prompt test.

3. Full-Context Trace Feedback: Replaces naive error truncations with sandbox-evaluated LHS/RHS runtime values for targeted self-repair.

☁️ Cloud Spot Deployment (Google Cloud / RunPod)

For larger models or massive multi-benchmark runs, we provide a self-deleting Google Cloud spot VM launcher with strict cost caps:

# Launches spot L4 GPU (g2-standard-8, ~$0.45/h), syncs results to bucket, and force-deletes on exit:
./deploy/run_on_gcp.sh --tag gcp_l4_n257 --n 257 --cap-usd 5.0

🧪 Open Call for Community Contributions (Humans & AI Agents)

We actively welcome contributions from human researchers, software engineers, and autonomous AI agents!

Top Priority Research Tracks:

1. Qwen (Gwen) Model Series Scaling:

   • Run scripts/run_benchmark.py on 0.5b, 3b, 7b, 14b, and 32b models and submit raw rows.jsonl and results.json pull requests.

2. Multi-Turn Exception Trace Self-Repair:

   • Enhance low_tier_engine.py to parse traceback line numbers and exception types into the repair prompt.

3. Formal Verification (Lean 4 Mathlib):

   • Extend the Lean oracle to automatically discover lake_packages and evaluate auto-formalization datasets (MiniF2F, ProofNet).

4. New Language Oracles:

   • Implement fail-closed compiler oracles for C++ (clang++), Go (go vet), and Julia.

5. AI Agent Pull Request Protocol:

   • If you are an AI coding agent (Claude Code, Antigravity, OpenHands), you are invited to fork this repo, implement an improvement, execute pytest tests/, verify git diff, and open an automated PR with full execution telemetry.

📜 Citation

If you use GWAYA in your research or applications, please cite the permanent Zenodo record:

@software{callens_2026_gwaya,
  author       = {Callens, Xavier},
  title        = {GWAYA v3.1.1: Fail-Closed Gate \& Real Toolchain Verification for LLM Code Generation},
  month        = oct,
  year         = 2026,
  publisher    = {Zenodo},
  version      = {3.1.1},
  doi          = {10.5281/zenodo.23123923},
  url          = {https://doi.org/10.5281/zenodo.23123923}
}

📄 License

This project is licensed under the MIT License.