Thaki-SecProof-4B-Preview
🇰🇷 한국어 카드: MODEL_CARD.ko.md
SecProof V1 PASS [single run] on a held-out sealed test that is synthetic code from the same generator (unseen template families, not real codebases), with one accepted protocol deviation (
retry_output_sha_mismatch, see the sealed section). Not production-ready and not validated for operational security use. The repository keeps its Preview name. The development-set numbers come from an in-distribution set built by the same synthetic generator as the training data. It is a single training run. Generalisation to independent code has not been verified, and the held-out sealed test (synthetic, unseen template families) was run once: PASS. See below.
A LoRA adapter for Qwen/Qwen3.5-4B 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. The sibling Thaki-SecProof-2B-Preview uses the same data, recipe, prompt format and output contract.
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-4B-Preview && cd Thaki-SecProof-4B-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). It is byte-identical to the 2B release 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.
Development-set results (seed 20261025, checkpoint step 750) [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.
| Metric | Stock Qwen3.5-4B | SecProof-4B-Preview |
|---|---|---|
| Required keys in order (T1 / T2 / T4 / T5) | 1.00 / 0.95 / 0.29 / 0.69 | 1.00 / 1.00 / 1.00 / 1.00 |
| Strict schema v2 (T1 / T2 / T4 / T5, diagnostic) | 0.00 / 0.45 / 0.00 / 0.00 | 1.00 / 1.00 / 1.00 / 1.00 |
| T1 balanced accuracy (3 verdicts) | 0.333 | 1.000 |
| T2 balanced accuracy | 0.339 | 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.957 | 0.000 |
| 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.224 | 1.000 |
Stock answered confirmed on all 124 T1 cases, which is why its balanced accuracy is 1/3 and its SAFE
false-confirm rate is high. 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 S, earliest step on ties):
| Step | 150 | 300 | 450 | 600 | 750 | 900 |
|---|---|---|---|---|---|---|
| S | 0.802 | 0.915 | 0.997 | 0.997 | 1.000 | 1.000 |
| SAFE false-confirm | 0.036 | 0.000 | 0.014 | 0.014 | 0.000 | 0.000 |
From step 450 on, S is at the ceiling of this dev set. One T1 case moves T1 balanced accuracy by roughly 0.008, so the differences between steps 450 and 900, and between this model (S = 1.000) and SecProof-2B-Preview (S = 0.997), are one or two cases. They are not evidence that 4B reviews real code better than 2B.
Sealed held-out evaluation: V1 PASS [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) | 1.000 | 0.338 | Δ CI95 lower > 0 (got +0.652) | pass |
| G2 vulnerable location correct (39) | 1.000 | 0.000 | ≥ 0.80 and ≥ stock | pass |
| G3 evidence pointing at non-existent code | 0.000 | – | ≤ 0.01 | pass |
| G4a decoy false confirm (239) | 0/239 = 0.000 (Wilson upper 0.016) | 0.979 | ≤ 0.15, upper ≤ 0.20, Δ CI95 upper ≤ 0 (got -0.959) | pass |
| 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 |
PASS. All eight gates passed. This is one training run scored once. It is still synthetic code from the same generator, so it says nothing about real codebases. On this result the owner approved the V1 label (2026-10-27); it means the pre-registered numeric gates were met, nothing more.
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.
- 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 isrejected(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 55629e36380f7592), 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. 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
| Item | Value |
|---|---|
| Base | Qwen/Qwen3.5-4B @ 851bf6e806efd8d0a36b00ddf55e13ccb7b8cd0a (Hub download byte-identical to the training copy; fingerprint 55629e36380f7592) |
| Base family | Qwen3.5 hybrid (Gated DeltaNet + attention), the same family as SecProof-2B. The 8B sibling, Thaki-SecProof-8B-Preview, uses a different base family (Qwen3-8B, dense attention), so results do not transfer between them by size alone |
| Method | LoRA r=16, alpha=32, dropout 0.05, all linear projections (32.5M 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 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, 7.14 s/step (median), 1.83 GPU-h training, peak 29.8 GiB |
| Adapter sha256[:16] | 4fb82ea048365729 |
| 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.5-4B is Apache-2.0; follow its terms as well.
Roadmap
Sealed evaluation done (above). The release decision is the owner's, alongside the 2B, 8B and 27B variants.