Thaki-SecProof-2B-Preview

Research Preview — SecProof V1 FAIL (G4a) [single run]. Not production-ready and not validated for operational security use. The development-set numbers come from an in-distribution set (same synthetic generator as training). A held-out sealed test (synthetic, unseen template families) was run once: FAIL. See below.

A LoRA adapter for Qwen/Qwen3.5-2B that audits small Python AI-agent runtimes for one of 12 named security boundaries and answers with a single, schema-fixed JSON finding: verdict, file/line evidence, severity, what is still unresolved, and (for patch tasks) a full-file patch.

Built by ThakiCloud as part of the SecProof model family (2B / 4B / 8B / 27B planned).

What it does

Task	Input	Output
T1 Discover	repository + one boundary	`confirmed` / `needs_validation` / `rejected` + evidence lines
T2 Verify	repository + a candidate finding	whether the candidate holds, with evidence
T4 Patch	repository + a confirmed issue	full-file patch + expected regression result
T5 Regression	repository + a candidate patch	whether the patch fixes the issue without breaking behaviour

Boundaries covered (and only these): approval_single_use, approval_tool_binding, cache_tenant_isolation, memory_trust_promotion, principal_confusion, rag_tenant_isolation, rag_write_tenant_binding, secret_exposure_output, tool_action_approval_binding, tool_authorization_scope, tool_identity, tool_tenant_binding.

Out of scope: general CVE hunting, memory-safety bugs, non-Python code, large real-world repositories, and any boundary not listed above. Expect unreliable output there.

Quick start

pip install "transformers>=5.0" "peft>=0.19" torch accelerate
git clone https://huggingface.co/ThakiCloud/Thaki-SecProof-2B-Preview && cd Thaki-SecProof-2B-Preview
python inference.py examples/t1_rag_tenant_isolation.json

secproof_prompt.py builds the exact prompt layout used in training (format v2: a TASK: line, an ordered OUTPUT KEYS line, the instruction, BOUNDARIES:, optional candidate/patch, then the repository rendered as numbered === path === blocks). Use it as is: the adapter was trained on this layout only. Decoding used for every number on this card: greedy, thinking off, max_new_tokens=2048.

Development-set results (seed 20261025, checkpoint step 750)

356 dev cases (T1 124, T2 92, T4 68, T5 72), scored by a deterministic scorer. "Stock" is the same base model with the same prompt and decoding, no adapter.

Metric	Stock Qwen3.5-2B	SecProof-2B-Preview
Output schema match (T1 / T2 / T4 / T5)	0.12 / 0.00 / 0.06 / 0.11	1.00 / 1.00 / 1.00 / 1.00
T1 balanced accuracy (3 verdicts)	0.258	0.992
T2 balanced accuracy	0.806	1.000
T4 patch both-pass in sandbox (security + functional tests)	0.00	1.00 (68/68)
SAFE false-confirm rate, T1+T2 (calling safe code vulnerable)	0.078	0.000
T1 vulnerable-location accuracy (diagnostic)	0.000	0.975
Evidence items pointing at non-existent code (diagnostic)*	0.000	0.000

* Only schema-valid outputs are location-graded, so stock's 0.000 reflects that most stock outputs were not gradeable.

Schema-invalid outputs are scored as wrong. Keys are never repaired after generation. Checkpoint 750 was chosen from 150/300/450/600/750/900 by a pre-registered rule (schema ≥ 0.99 per task, then SAFE false-confirm ≤ stock, then highest mean of T1 bacc, T2 bacc, T4 both-pass, earliest step on ties). Step 900 tied with 750.

Limitations (read before using these numbers)

In-distribution only. Dev cases come from the same synthetic generator and the same 12 boundaries as the training data. Exact-code and identifier-stripped skeleton duplicates between train and dev are 0, and the generated repositories (worlds) are disjoint (train 487, dev 44, shared 0), but all 14 bug templates and all 12 boundaries appear in both. That is not distribution independence. These numbers show the model learned this task family; they are not evidence of generalisation to new code patterns.
The sealed test is synthetic too. It holds out template families but uses the same generator; passing or failing it is not evidence about real codebases.
T4/T5 verdicts carry a task-type cue. In this data every T4 gold verdict is confirmed (68/68) and every T5 gold verdict is rejected (72/72), so those verdicts can be guessed from the task name. For T4 the meaningful metric is the sandbox both-pass rate, not verdict accuracy.
Much of the gain over stock is format. Stock rarely produces the required schema (and hit the 2048-token limit on 51/356 cases). Format-independent signal is T1 balanced accuracy and location accuracy.
One training run. This preview is a single run (seed 20261025). Seed variance is not measured; quality will be judged by independent evaluation rather than repeated seeds.
Synthetic, small repositories. Real codebases are larger, messier and multi-language.
Do not use this model as the sole basis for a security decision. Treat findings as leads for a human reviewer.

Sealed held-out evaluation: V1 FAIL (G4a) [single run]

Run once on 2026-10-26, after every family member was selected, with gates fixed beforehand. The sealed set holds out 6 of the generator's 60 template families from training and dev: T1 327 cases (127 sealed: 39 vulnerable, 39 already fixed, 39 decoys, 10 undecidable; plus 200 extra decoys) and T4 39 patch cases. "Stock" is the same base model with the same prompt, median of three greedy runs.

Gate	This adapter	Stock	Rule	Result
G1 T1 verdict, balanced accuracy (sealed 127)	0.966	0.271	Δ CI95 lower > 0 (got +0.617)	pass
G2 vulnerable location correct (39)	0.923	0.000	≥ 0.80 and ≥ stock	pass
G3 evidence pointing at non-existent code	0.000	–	≤ 0.01	pass
G4a decoy false confirm (239)	5/239 = 0.021 (Wilson upper 0.048)	0.050	≤ 0.15, upper ≤ 0.20, Δ CI95 upper ≤ 0 (got +0.004)	FAIL
G4b already-fixed code called vulnerable (39)	0/39 = 0.000	–	≤ 0.10	pass
G5 undecidable cases answered `needs_validation` (10)	10/10	–	≥ 0.70	pass
G6 T4 patch passes sandbox security + functional tests (39)	1.000	0.000	≥ 0.70 and Δ CI95 lower > 0	pass
G7 output format (sealed T1 / T4)	1.0 / 1.0	–	≥ 0.99	pass

FAIL. It fails only the stock-comparison part of G4a: the decoy false-confirm level (0.021) and its Wilson upper bound (0.048) are within the limits, but stock Qwen3.5-2B itself rarely confirms decoys (0.050), so the adapter is not shown to be better than stock on this gate. This is one training run scored once. It is still synthetic code from the same generator, so it says nothing about real codebases. The owner kept this model as a Research Preview (2026-10-27); it will not be retrained.

Sealed results for the family: 2B FAIL (G4a), 4B PASS, 8B FAIL (G4b), 27B V1 PASS (Thaki-SecProof-27B-V1).

Protocol deviation (retry_output_sha_mismatch). The pre-registration required that any infrastructure rerun reproduce byte-identical outputs. The first sealed submission of every family member stopped before producing any output (a bug in our job); the 2B job then needed one more rerun, and its outputs were not byte-identical to the interrupted run (the 2B adapter's parsed verdicts matched 366/366; stock runs differed more). The owner accepted this deviation on 2026-10-27. Only complete runs were scored, each once. The original rule is kept as written and is not marked as met.

Out-of-distribution spot check (known miss)

examples/t1_rag_tenant_isolation.json is a small hand-written repository, not produced by the training generator. search.find(tenant, query) ignores tenant, so one tenant can read another tenant's documents: the correct answer is confirmed at app/search.py:10.

The preview answers rejected. It points at the right line, but its rationale claims the search filters by tenant, which the code does not do. The output is valid JSON with the expected keys, so the format generalises, but the judgement does not. This is the kind of failure the dev numbers above cannot show. Keep a human reviewer in the loop.

Training

Item	Value
Base	`Qwen/Qwen3.5-2B` @ `15852e8c16360a2fea060d615a32b45270f8a8fc` (byte-identical to the training copy; file fingerprint `dae3c7ee678107dc`)
Method	LoRA r=16, alpha=32, dropout 0.05, all linear projections
Optimiser	lr 1e-4, cosine, warmup 3%, grad clip 1.0, effective batch 8 (2 per task), max seq 8192
Loss	cross-entropy on the assistant JSON tokens only
Steps	900 (checkpoint 750 released)
Data	3,556 synthetic training records (T1 1,289 · T2 933 · T4 617 · T5 717), generated in-house; patch labels from sandbox execution
Hardware	1× NVIDIA H200 NVL, 4.28 s/step, 1.195 GPU-h training, peak 24.7 GiB
Adapter sha256[:16]	`71e73f47266250e8`
Code version	internal commit `f2eba5eb51` · `secproof_sft_v1_job.py` `60232d2f24d13642` · `sft_format.py` `2367ca36aeb350dc`

The training and evaluation data are not released. They were generated by an in-house synthetic generator (no third-party source code, no personal data).