ThakiCloud

Thaki-SecProof-8B-Preview

README

License: apache-2.0

What it does

Table with columns: Task, Input, Output
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

bash

pip install "transformers>=5.0" "peft>=0.19" torch accelerategit clone https://huggingface.co/ThakiCloud/Thaki-SecProof-8B-Preview && cd Thaki-SecProof-8B-Previewpython 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). It is byte-identical to the 2B and 4B releases and was checked against the training renderer on all 356 dev cases (356/356 identical). 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. bf16 weights need roughly 17 GB of GPU memory.

Development-set results (seed 20261025, checkpoint step 450) [single run]

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.

Table with columns: Metric, Stock Qwen3-8B, SecProof-8B-Preview
Metric	Stock Qwen3-8B	SecProof-8B-Preview
Required keys in order (T1 / T2 / T4 / T5)	1.00 / 1.00 / 1.00 / 0.97	1.00 / 1.00 / 1.00 / 1.00
Strict schema v2 (T1 / T2 / T4 / T5, diagnostic)	0.00 / 1.00 / 0.00 / 0.00	1.00 / 1.00 / 1.00 / 1.00
T1 balanced accuracy (3 verdicts)	0.292	0.983
T2 balanced accuracy	0.736	0.988
T4 patch both-pass in sandbox (security + functional tests)	0.00	1.00 (68/68)
SAFE false-confirm, T1+T2 (calling safe code vulnerable)	72/141 (0.511)	4/141 (0.028)
T1 vulnerable-location accuracy (diagnostic)	0.000	1.000
Evidence items pointing at non-existent code (diagnostic)	0.000	0.000
Selection objective S (mean of T1 bacc, T2 bacc, T4 both-pass)	0.343	0.9903

Stock Qwen3-8B answered needs_validation on all 68 T4 cases and on 67 of 72 T5 cases, so its patch tasks score zero. Schema-invalid outputs are scored as wrong. Keys are never repaired after generation.

Where this checkpoint is wrong on dev

Two different error types are reported separately, because they cost different things in practice:

Table with columns: Error, What it means, Dev count (Wilson 95% CI)
Error	What it means	Dev count (Wilson 95% CI)
SAFE false-confirm, decoy	code that looks risky but is guarded, called `confirmed`	3/69 (0.043; 0.015–0.120), all T1
SAFE false-confirm, fixed	already-fixed code called `confirmed`	1/72 (0.014; 0.002–0.075), T1
Missed vulnerability (False SAFE)	vulnerable code not called `confirmed`	1/67, T2

The four false confirms are in tenant_arg_override (2), wrong_principal_scope (1) and memory_untrusted_promotion (1) cases. A false confirm sends a reviewer to look at safe code; a missed vulnerability is the more dangerous error, and it is a separate line above. The SecProof-4B-Preview release had 0/141 and 0/67 on the same dev set. With one run and these counts, that gap is not a reliable ranking either way.

The pre-registered decoy false-confirm gate (G4a) is defined on the sealed decoy set (239 SAFE_DECOY cases), not on dev. It was run once with the other sealed gates (see below). The dev decoy count above uses the same definition (share of SAFE_DECOY answered confirmed) on the 69 dev decoys only.

Checkpoint selection

Step 450 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 S, earliest step on ties):

Table with columns: Step, 150, 300, 450, 600, 750, 900
Step	150	300	450	600	750	900
S	0.783	0.889	0.990	0.990	0.989	0.989
T1 balanced accuracy	0.363	0.708	0.983	1.000	0.996	0.996
T4 both-pass	1.000	0.971	1.000	0.971	0.971	0.971
SAFE false-confirm	0.007	0.000	0.028	0.000	0.007	0.007

Steps 450 and 600 differ in S by 0.0001, less than one case. Step 450 is better on T4 (68/68 vs 66/68); step 600 is better on T1/T2 verdicts and has no SAFE false confirms. Which one does better on real code is unknown. The rule picked 450 and the choice was not revisited after seeing the numbers.

All six checkpoints pass the format bar. An earlier 30-step smoke run of the 8B recipe failed the T4 format check (2/68 schema-valid patches); that was an early, unconverged checkpoint, and the 900-step run above is the one released.

Sealed held-out evaluation: V1 FAIL (G4b) [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.

Table with columns: Gate, This adapter, Stock, Rule, Result
Gate	This adapter	Stock	Rule	Result
G1 T1 verdict, balanced accuracy (sealed 127)	0.957	0.453	Δ CI95 lower > 0 (got +0.455)	pass
G2 vulnerable location correct (39)	1.000	0.000	≥ 0.80 and ≥ stock	pass
G3 evidence pointing at non-existent code	0.002	–	≤ 0.01	pass
G4a decoy false confirm (239)	30/239 = 0.126 (Wilson upper 0.173)	0.506	≤ 0.15, upper ≤ 0.20, Δ CI95 upper ≤ 0 (got -0.298)	pass
G4b already-fixed code called vulnerable (39)	4/39 = 0.103	–	≤ 0.10	FAIL
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 G4b: 4 of 39 already-fixed cases were called vulnerable (limit: 3). This is the same weakness seen on dev (safe-code false confirms), larger on the held-out families. 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.

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.
Bigger is not shown to be better. SecProof-4B-Preview scored S = 1.000 and this model 0.990 on the same dev set. The gap is five dev cases (four false confirms, one miss) and does not show that either size is the right choice for real code.
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). For T4 the meaningful metric is the sandbox both-pass rate.
One training run. Seed variance is not measured.
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, and verify any fix in a sandbox before applying it.

Release check and one example outside the generator

Before publishing, a fresh GPU job downloaded the base model from the Hub at the pinned revision, loaded this repository's adapter and ran it. The downloaded base files are byte-identical to the copy used in training (file fingerprint cc30eb294736cccd), and the adapter file matches the hash below. Nine inference runs (two per task plus the example) all produced schema-valid format v2 JSON, and on the eight dev cases each verdict matched the development-set run.

examples/t1_rag_tenant_isolation.json was written by hand, not by the synthetic generator. Its expected answer is confirmed with evidence at app/search.py line 10, where the search ignores the tenant argument. This adapter answered confirmed, boundary rag_tenant_isolation, evidence app/search.py:10, the same answer as SecProof-4B-Preview. SecProof-2B-Preview answered rejected on the same file. This is one case. It shows the release loads and runs; it is not a generalisation result.

Training

Table with columns: Item, Value
Item	Value
Base	`Qwen/Qwen3-8B` @ `b968826d9c46dd6066d109eabc6255188de91218` (Hub download byte-identical to the training copy; fingerprint `cc30eb294736cccd`)
Base family	Qwen3 dense attention. SecProof-2B and 4B use Qwen3.5 hybrid (Gated DeltaNet + attention); results do not transfer between them by size alone
Method	LoRA r=16, alpha=32, dropout 0.05, all attention and MLP projections (43.6M trainable parameters)
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 450 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, 9.73 s/step (median), 2.47 GPU-h training, peak 30.0 GiB
Adapter sha256[:16]	`4acda582bb4fbaa0`
Code version	`secproof_sft_v1_job.py` `3be200db31a11e38` · `sft_format.py` `2367ca36aeb350dc`

Data and rights

The training and evaluation data are not released. Repositories are produced by an in-house deterministic generator (no third-party source code; every secret-looking value is a fake FAKE-TENANT-* token; no personal data). Labels come from the generator's ground truth and sandbox execution, not from a model. Free-text rationales were written by an in-house quantised Qwen-family teacher model and kept only when its verdict, boundary and location matched the ground truth. The teacher prompt drew on the MIT-licensed cloudflare/security-audit-skill guidance. That text is not part of this repository.

License

Adapter weights and code in this repository: Apache-2.0. The base model Qwen/Qwen3-8B is Apache-2.0; follow its terms as well.

Roadmap

Sealed evaluation done (above). The release decision is the owner's, alongside the 2B, 4B and 27B variants.

Available on FriendliAI

Dedicated Endpoints

Run this model inference on single tenant GPU with unmatched speed and reliability at scale.

Learn more

Model Details

Model Provider

ThakiCloud

Model Tree

Base

Qwen/Qwen3-8B

Adapter

this model

Input Modalities

Text

Output Modalities