VeriKernel

Faster code is worthless if the physics is wrong. VeriKernel uses NVIDIA Nemotron on Nebius & Tavily to autonomously optimize C++ kernels with mathematical determinism and Navier-Stokes verification.

Comment

Inspiration

Modern LLMs and deep reasoning models are remarkably adept at generating high-performance code. When asked to accelerate computational loops, models like NVIDIA Nemotron frequently emit #pragma omp parallel for or aggressive compiler flags like -ffast-math.

The generated code compiles cleanly, and naive microbenchmarks report eye-popping 5× to 13× speedups. However, beneath the surface, loop-carried dependencies introduce silent data races and floating-point drift. The resulting fluid simulations and wave propagations produce divergent values across thread counts and violate conservation laws.

In high-performance scientific computing and mission-critical engineering, faster code is completely worthless if the physics is wrong.

We built VeriKernel to close this trust gap: an automated HPC verification engine and agentic self-correction harness that treats LLM-generated code not as trusted output, but as a candidate needing empirical and mathematical cross-examination against ground truth.

What It Does

VeriKernel operates an immutable 5-Stage Physics & Determinism Referee Gate paired with an autonomous NVIDIA Nemotron-3 + Tavily repair loop:

  1. Stage 1 (Static Allow-List Linter): Blocks unauthorized system calls, forbidden headers, and unsafe floating-point pragmas (#pragma GCC optimize("fast-math")).
  2. Stage 2 (Hardened Sandboxed Build): Compiles the mutable candidate kernel against an immutable test harness inside a resource-constrained container using GCC with strict OpenMP flags.
  3. Stage 3 (Differential Multi-Thread Determinism Gate): Executes sweeps across $T \in {1, 2, 4, 8}$ threads. If run-to-run cross-thread divergence exceeds $\Delta > 10^{-11}$, the kernel is rejected for race conditions (RACE_NON_DETERMINISTIC) without the memory bloat of ThreadSanitizer.
  4. Stage 4 (Navier-Stokes Physics & Ghia $L_2$ Oracle): Simulates a 2D Lid-Driven Cavity ($\text{Re}=100$, $129 \times 129$ grid) until steady state. Checks relative $L_2$ error against precomputed reference binaries ($\le 10^{-5}$) and compares centerline velocity profiles against the 17 empirical benchmark points of Ghia, Ghia, & Shin (1982) ($\text{RMSE} \le 0.05$).
  5. Stage 5 (Pinned Out-of-L2 Bandwidth Benchmark): Measures median runtime and memory throughput on an out-of-L2 $513 \times 513$ grid with hardware core pinning (OMP_PROC_BIND=close, OMP_PLACES=cores).

When a candidate fails, VeriKernel triggers Load-Bearing Tavily Search keyed to the exact failure signature. Search results and compiler/telemetry diagnostics are injected into the retry prompt, enabling NVIDIA Nemotron-3 on Nebius Token Factory to autonomously refactor lexicographical loops into race-free Red-Black Gauss-Seidel stencils with AVX vectorization.

How We Built It

  • Model Engine: nvidia/nemotron-3-super-120b-a12b hosted on Nebius Token Factory, providing deep multi-core algorithmic reasoning at \$0.30/M input and \$0.90/M output tokens.
  • Diagnostic Information Retrieval: Tavily Search API, triggered strictly upon referee failure to retrieve OpenMP specifications and cache-blocking stencil patterns.
  • HPC Simulation Harness: Modern C++17 with OpenMP 4.5/5.0, AVX intrinsics, and dual-grid solvers for the 2D Navier-Stokes Lid-Driven Cavity and 2D Acoustic Wave Equation.
  • Execution & Sandboxing: Containerized execution with cgroup limits, PID isolation, and an asyncio.Lock() queue protecting dedicated CPU cores.
  • Lab-Instrument Frontend: Dark graphite web interface featuring an Attempt Ladder with side-by-side Monaco code diffs, interactive Ghia centerline velocity curves, a Break-It Gallery, and one-click cryptographic verification certificate export.
  • 3-Tier High-Availability Architecture:
    • Tier 1: Live 8-core virtual machine with rate-limiting and daily spend caps.
    • Tier 2: Persistent HTTPS ingress via secure tunnel.
    • Tier 3: Zero-backend static edge mirror on GitHub Pages with 100% historical telemetry and full interactive diffs.

Empirical Benchmark Study ($N=30$)

We conducted an empirical benchmark comparing standard Ungated One-Shot Generation (Arm A) against VeriKernel's Gated Retry Loop (Arm B) across 3 prompt styles $\times$ 10 stochastic trials ($N=30$ runs):

Metric Arm A: One-Shot Ungated Arm B: VeriKernel Gated Loop Impact
Verification Pass Rate 13.3% (4/30) 93.3% (28/30) +80.0% reliability gain
Local Compiler Failures (Stage 2) 25/30 runs 2/30 runs (only after 4 retries) Compiler-in-the-loop eliminates loop syntax defects
Physics / Invariant Drift (Stage 4) 1/30 runs (silent race) 0/30 runs Zero unphysical speedups slip through
Genuine Algorithmic Defect Rate 96.2% (25/26 failed runs) 0.0% (0/2 failed runs) Arm B only failed on context token truncation
Median Verified Speedup N/A (13% sample) 13.66× over baseline Peak: 20.86× (437.5 GB/s in L3 cache)
Mean Inference Cost per Run \$0.0060 USD \$0.0115 USD Just +$0.0055 for guaranteed correctness
True Cost per Usable Kernel \$0.0449 USD \$0.0123 USD VeriKernel is 3.6× cheaper per valid asset

🥊 Break-It Gallery (Zero-Token Adversarial Verification)

To prove that our referee isolates bugs deterministically without wasting LLM tokens, we created an adversarial gallery of 6 defective kernels:

  1. bug_1_fast_mathcheat.hpp: Sneaked fast-math pragma $\rightarrow$ Caught by Stage 1 Linter.
  2. bug_2_naive_omp_race.hpp: Race condition in Gauss-Seidel ($\Delta = 3.87 \times 10^{-5}$) $\rightarrow$ Caught by Stage 3 Determinism Gate.
  3. bug_3_boundary_off_by_one.hpp: Momentum severed from cavity lid (RMSE 0.3872) $\rightarrow$ Caught by Stage 4 Physics Gate.
  4. bug_4_fp32_downgrade.hpp: Stalled residual above tolerance $\rightarrow$ Caught by Stage 4 Physics Gate.
  5. bug_5_wrong_redblack_index.hpp: 1D stride parity error (fake 13.3× speedup, 99% error) $\rightarrow$ Caught by Stage 4 Physics Gate.
  6. bug_6_wave_naive_startup.hpp: 1st-order startup degrading wave convergence ($p=1.008 < 1.90$) $\rightarrow$ Caught by Stage 4 Wave Gate.

Challenges We Ran Into

  1. OpenMP §2.6 Canonical Loop Rules: Nemotron frequently emitted for (size_t i = 1; i + 1 < n; ++i). While valid standard C++, OpenMP specifications require canonical controlling predicates (var < ub). Without compiler feedback, Arm A failed 83% of the time on this single error. Stage 2 compiler telemetry resolved this immediately.
  2. Reasoning Token Ceilings: Deep reasoning models emit internal Chain-of-Thought (CoT) before outputting code. An initial max_tokens=2500 ceiling led to token starvation mid-header. Expanding to max_tokens=16384 allowed full reasoning and emission, unlocking our 93.3% pass rate.
  3. Core Pinning on Virtualized Hardware: Virtual CPU migrations caused high runtime jitter. Enforcing OMP_PROC_BIND=close and OMP_PLACES=cores pinned threads to physical cores, yielding deterministic nanosecond timing.

What We Learned

  • Compiler & Telemetry Reflection is Mandatory: LLMs cannot optimize scientific HPC loops reliably without compiler diagnostics in the feedback loop. 25 of 26 one-shot failures were eliminated solely by returning GCC error logs to the model.
  • Differential Determinism Beats Sanitizers: Running multi-threaded sweeps ($1, 2, 4, 8$ threads) across identical seeds and asserting $\Delta \le 10^{-11}$ catches race conditions faster and with zero runtime memory bloat compared to heavyweight tools like ThreadSanitizer.
  • The Economic Inversion of Autonomous Verification: While multi-turn self-correction costs slightly more per raw attempt (\$0.0115 vs \$0.0060), it is 3.6× cheaper per usable production kernel (\$0.0123 vs \$0.0449) because 86.7% of ungated code is unusable broken junk.

Accomplishments We're Proud Of

  • Zero Unrecovered Code Defects in Arm B: Every algorithmic and syntax failure caught by the referee was repaired by the Nemotron + Tavily loop.
  • Mathematical Grounding: We evaluate code against Navier-Stokes conservation invariants and Ghia et al. (1982) peer-reviewed experimental fluid dynamics, not just regexes or mock test cases.
  • Zero-Backend Edge Mirror: Guaranteeing 100% judge availability with an interactive static mirror that never goes down.

What's Next for VeriKernel

  • Multi-GPU Kernels: Extending the referee to NVIDIA CUDA kernels using cuBLAS/cuFFT ground-truth invariants.
  • Formal Verification Integration: Coupling the determinism checker with LLVM Polly polyhedral analysis for compile-time loop-dependency proofs.
  • Distributed HPC Scaling: Testing MPI domain decomposition across multi-node Nebius cloud clusters.

Built With

  • agentic-ai
  • ai-agents
  • asyncio
  • avx2
  • benchmarking
  • c++
  • docker
  • fastapi
  • fluid-dynamics
  • github
  • high-performance-computing
  • llm
  • monaco-editor
  • navier-stokes
  • nebius-ai-cloud
  • nebius-token-factory
  • ngrok
  • nvidia-nemotron
  • openmp
  • python
  • scientific-computing
  • simd
  • tavily-search-api
  • verification
Share this project:

Updates

Submission history