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
pip install "transformers>=5.0" "peft>=0.19" torch accelerate# optional, much faster on the linear-attention layers: pip install flash-linear-attention causal-conv1dgit clone https://huggingface.co/ThakiCloud/Thaki-SecProof-27B-V1 && cd Thaki-SecProof-27B-V1python inference.py examples/t1_rag_tenant_isolation.json
secproof_prompt.py builds the exact prompt layout used in training (format v2). It is byte-identical to the 2B, 4B
and 8B releases. Use it as is: the adapter was trained on this layout only. Decoding for every number on this card:
greedy, thinking off, max_new_tokens=2048. The bf16 base needs roughly 55 GB of GPU memory; our batch-4 generation
runs peaked at 59.8 GiB.
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.
Table with columns: Gate, This adapter, Stock, Rule, Result| Gate | This adapter | Stock | Rule | Result |
|---|
| G1 T1 verdict, balanced accuracy (sealed 127) | 1.000 | 0.342 | Δ CI95 lower > 0 (got +0.645) | 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.912 | ≤ 0.15, upper ≤ 0.20, Δ CI95 upper ≤ 0 (got -0.875) | 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 PASS.
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), and the 2B job later needed one more rerun. The 2B rerun's outputs were not byte-identical to the interrupted run (the 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 27B sealed outputs come from a single complete run. The original rule is kept as written, not marked as met.
Development-set results (seed 20261025, checkpoint step 300) [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.8-27B, SecProof-27B-V1| Metric | Stock Qwen3.8-27B | SecProof-27B-V1 |
|---|
| Required keys in order (T1 / T2 / T4 / T5) | 0.38 / 0.91 / 0.62 / 0.79 | 1.00 / 1.00 / 1.00 / 1.00 |
| T1 balanced accuracy (3 verdicts) | 0.358 | 1.000 |
| T2 balanced accuracy | 0.945 | 1.000 |
| T4 patch both-pass in sandbox (security + functional tests) | 0.00 | 1.00 (68/68) |
| SAFE false-confirm, T1+T2 (calling safe code vulnerable) | 74/141 (0.525) | 0/141 |
Missed vulnerability, T1+T2 (vulnerable code not called confirmed) | 4/67 | 0/67 |
| T1 vulnerable-location accuracy (diagnostic) | 0.000 | 1.000 |
| Selection objective S (mean of T1 bacc, T2 bacc, T4 both-pass) | 0.434 | 1.000 |
Stock Qwen3.8-27B answered confirmed on 116 of 124 T1 cases and its output breaks the strict schema, so it scores near zero on location and patch tasks.
Checkpoint selection
Step 300 was chosen from 150–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.9972 | 1.0000 | 1.0000 | 1.0000 | 1.0000 | 1.0000 |
| T1 balanced accuracy | 0.992 | 1.000 | 1.000 | 1.000 | 1.000 | 1.000 |
| SAFE false-confirm | 0.000 | 0.000 | 0.000 | 0.000 | 0.000 | 0.000 |
Five of the six checkpoints reach S = 1.000 with no false confirms, so on dev this model is at the ceiling and the dev set cannot tell those checkpoints apart. Step 300 was picked by the pre-registered tie rule (earliest step), not because it is known to be better than 450–900.
Limitations (read before using these numbers)
- Synthetic only. Dev and sealed cases both come from the same in-house generator and the same 12 boundaries. The
sealed set holds out 6 of 60 template families, which is stronger than dev, but it is still not real code.
- Ceiling. The adapter scores 1.000 on almost every dev and sealed metric, as does SecProof-4B. These sets cannot
rank 4B against 27B; choose between them on your own code.
- One training run, scored once. Seed variance is not measured.
- T4/T5 verdicts carry a task-type cue. Every T4 gold verdict is
confirmed and every T5 gold verdict is
rejected. For T4 the meaningful metric is the sandbox both-pass rate.
- Known weak spot in the family. In a product test on a hand-built repository whose tenant isolation depends on
facts not in the code, the 2B, 4B and 8B models all answered
confirmed where needs_validation was expected.
Keep a sandbox or a human between this model and any action.
- 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 rebuilt the base model at the pinned revision and loaded this repository's adapter.
Because the base is 54 GB, it was taken from our mirror and checked file by file against the Hub revision: all 32 files
present, 19 large files matching the Hub's published SHA-256, the rest byte-identical (file fingerprint 7302d6b2f9de96ac, the same
as in training). The adapter file matches the hash below. Nine inference runs (two per task plus the example) all
produced schema-valid format v2 JSON, the bundled inference.py ran end to end, 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, as SecProof-4B and 8B did;
SecProof-2B answered rejected. 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.8-27B @ 1d4bf0f2ff6012fd82039f2fa52739d0dd7c60c0 (mirror verified file by file against the Hub revision; fingerprint 7302d6b2f9de96ac) |
| Method | LoRA r=16, alpha=32, dropout 0.05, all linear projections in attention, linear-attention and MLP blocks (116.8M 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 300 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 B200, 19.35 s/step (median), 4.94 GPU-h training, peak 76.7 GiB |
| Adapter sha256[:16] | 782c9e8e92eae4bf |
| 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.8-27B is Apache-2.0; follow its terms as well.