Inspiration
AI can rewrite a service in minutes, but speed creates a new review problem: how do we prove that rounding, error behavior, status codes, and test coverage survived the migration? A plausible answer is not enough for a private codebase. We built ProofEdge to make every useful AI suggestion traceable—and every performance claim falsifiable.
What it does
ProofEdge is a local-first migration-assurance agent. It compares source and target repositories without executing them, maps public contracts, identifies semantic and coverage risks, checks declared migration claims, and asks a compact local model to rank migration risks.
The model is not the authority. A deterministic AST/OpenAPI compiler turns selected risks into a small executable differential-testing plan with explicit source-versus-target purpose and visible file-and-line evidence. Semantic, provenance, and risk gates decide what may be published. Raw model wording is retained for audit but cannot directly become a final claim.
The public demo replays a frozen refund migration where an optional argument disappears while the migration still claims compatibility. ProofEdge cites the source and target evidence, proposes the boundary test, and refuses the unsupported claim. Private code stays on the Arm64 machine: the demo uploads nothing and uses no hosted model API.
How we built it
The core is a Python 3.11 package with:
- a bounded, non-executing repository scanner
- deterministic contract and claim analysis
- evidence-selected context
- a strict loopback-only local-model client
- objective-based model evaluation
- a deterministic proposal compiler
- Markdown and JSON evidence-ledger reporting
Repository instruction-like text is replaced with typed hash placeholders before inference. The loopback client disables proxies, redirects, prompt caching, non-loopback DNS targets, and oversized responses. Compiler provenance records whether each selected risk was model-aligned or restored by a deterministic safety floor.
The inference path pins llama.cpp, Qwen2.5-Coder-1.5B-Instruct Q4_0, and model bytes by SHA-256. For Arm optimization we compiled the exact same runtime twice, with KleidiAI disabled and enabled. A predeclared exploratory sweep selected four threads, chunk multiplier 1, batch 1024, and micro-batch 256. We committed that profile before launching the independent confirmation.
Arm64 optimization and measured evidence
The confirmation ran on a genuine aarch64 Neoverse N2 GitHub runner. Four fresh processes executed in ABBA order. Source, model, quantization, VM, workload, and thread count stayed fixed; only GGML_CPU_KLEIDIAI changed. Runtime logs proved selection of the I8MM Q4 kernel.
- pp1024: 96.6036 → 97.1860 tokens/s, +0.6029%
- tg128: 34.7734 → 36.9914 tokens/s, +6.3783%
All four baseline/optimized × KleidiAI-off/on quality configurations passed both frozen cases. Compiled-reference validity, semantic-objective coverage, and risk-evidence coverage were 1.00, with zero canary leakage and zero fallback. Raw-model reference validity is disclosed separately at 0.50 baseline and 0.75 KleidiAI. We retained the first mixed profile and four failed semantic canaries instead of hiding them.
The complete two-case product task was repeated five times per build and every run passed. Published compiled-plan hashes were identical across builds. Task p50 changed from 45.387 to 44.639 seconds (-1.648%), streamed TTFT p50 from 14.960 to 14.867 seconds (-0.622%), and request p50 from 22.674 to 22.314 seconds (-1.587%). Raw model outputs and completion-token counts differed, so these product timings are descriptive; we do not claim exact isolated-kernel attribution from them.
No energy claim is made. Raw JSON, stderr, CMake caches, binary identities, environment metadata, quality ledgers, and 81 independently verified SHA-256 entries are public.
Why ProofEdge should win
ProofEdge makes optimization evidence part of the product contract. A faster runtime cannot ship unless the same frozen migration objectives, exact evidence references, injection canaries, and fallback rules still pass.
Judges can inspect the first negative result, four failed semantic canaries, the predeclared tuning policy, runtime I8MM proof, stable compiled product plans, raw model divergence, and every raw hash. This turns an Arm kernel improvement into a trustworthy private-AI workflow instead of a benchmark screenshot.
The product matters beyond this challenge: migration review is privacy-sensitive, expensive to outsource, and unusually vulnerable to plausible unsupported claims. CPU-only Arm64 inference keeps source local, while ProofEdge's deterministic gates make a compact model useful without making it authoritative.
Challenges we ran into
The hardest part was resisting convenient but invalid comparisons. Identical model bytes do not prove identical useful output, repeated samples inside one process are not independent hosts, and build-time KleidiAI enablement does not prove that an Arm kernel ran.
An independent audit also showed that valid citations can support semantically useless tests. We responded with separate quality objectives, process-level ABBA blocks, runtime-log gates, a deterministic proposal compiler, and an explicit selection-versus-confirmation boundary.
Untrusted repositories created a second challenge. We hardened directory traversal, local HTTP, schema validation, report rendering, prompt-injection handling, and fallback attribution, then added adversarial tests instead of relying on the prompt alone.
Accomplishments that we are proud of
- A useful local-first product, not a benchmark wrapper
- A positive final Arm64 run after publishing an earlier negative result and four failed canaries
- Quality gates that vetoed apparently faster runtimes four times before release
- 57 automated tests and more than 85% Python coverage
- Pinned CI actions, hash-locked development dependencies, and zero production npm-audit findings
- A public demo, evidence bundle, threat model, and reproducible Arm64 build path
What we learned
Optimization evidence is strongest when every layer has a name and a boundary: kernel, serving profile, model quality, and product workflow. Arm-specific kernels matter, but the release gate is what makes the result trustworthy. Small local models become far more useful when deterministic evidence constrains their authority.
What's next
We plan to add larger pre-frozen migration corpora, process-level repetition across several native hosts, safe user-approved test execution, and energy measurements only on calibrated hardware.
Log in or sign up for Devpost to join the conversation.