DEV Community: GeneLab_999

Proving what a URL allowlist decides, in Lean 4

GeneLab_999 — Wed, 28 Oct 2026 17:46:41 +0000

This article describes URLFence as of commit ea3c061 (CI: run 40618042270).

AI agents fetch web pages for you, and their tools are supposed to stay on an allowlist of hosts.
That kind of check ("is this URL's host allowed?") keeps going wrong in the same few ways, in agent
tools and elsewhere:

A string prefix or suffix instead of a hostname comparison.
- CVE-2026-24052 (Claude Code WebFetch before 1.0.111) and CVE-2026-46341 (Apify MCP server before 0.9.21) used startsWith, so modelcontextprotocol.io.example.com and docs.apify.com.evil.com passed.
- CVE-2026-33393 (Discourse's spam-host allowlist) used end_with? without a dot boundary, so attacker-example.com passed.
Userinfo taken for the host: CVE-2025-47241 (browser-use before 0.1.45).
Normalising before checking: CVE-2026-6322 (fast-uri before 3.1.2) decoded a percent-encoded @.

URLFence (https://github.com/hiroki-abe-58/urlfence) is a small Lean 4 library and CLI that makes
this decision, with theorems about what it decides.

What it does

$ .lake/build/bin/urlfence check --allow docs.python.org --allow '*.example.com' -- https://docs.python.org/3/ https://docs.python.org.evil.com/ https://docs.python.org@evil.com/
{"input":"https://docs.python.org/3/","decision":"allow","scheme":"https","host":"docs.python.org","port":null}
{"input":"https://docs.python.org.evil.com/","decision":"deny","scheme":"https","host":"docs.python.org.evil.com","port":null}
{"input":"https://docs.python.org@evil.com/","decision":"reject","reason":"userinfo"}

It fails closed. It accepts only a strict, canonical form of http(s) URLs and refuses
everything else with a reason:

whitespace, backslashes and non-ASCII characters;
uppercase letters in the scheme or host;
userinfo and percent signs in the authority;
IPv6 literals and IDNA xn-- labels;
browser-style shortcuts like https:/x, 127.1 or 0x7f.0.0.1.

That costs some convenience. In exchange, an accepted URL leaves little room for a second reading:
the proofs pin how URLFence reads it, and a test checks that Node's WHATWG parser agrees.

The theorems

parse_authority: in an accepted URL, the text from // up to the first /, ?, # or the end is exactly the host followed by an optional :port. isDelim_iff pins those three characters.
parseHost_chars: the host contains only a-z, 0-9, - and ., so it has no @, : or brackets to confuse anyone.
sub_matches_iff_render: a *.example.com pattern matches exactly when the host ends with . followed by example.com, which is the dot boundary the suffix bugs missed.
check_allow_iff: a URL is allowed iff it parses, its scheme is allowed, it matches an allowed pattern, and it matches no denied pattern.

The audit script requires 55 published theorems by name (22 for URLs, 33 for the address check
below). All of them depend only on Lean's standard
axioms, and each one is pinned together with the library definitions it depends on. The audit also
replays every module through Lean's kernel checker.

Tested against real parsers

The proofs are about URLFence's own parser. Whether a browser-grade parser reads the URL the same way
is a tested claim, not a proven one:

A differential test runs about 10,000 random and adversarial URLs, including printable ASCII characters inserted into hosts at random positions.
For every URL URLFence accepts, Node's WHATWG URL must report the same scheme, host and port, and no userinfo.
tests/compat.py goes further, on a fixed corpus of 41,647 boundary-heavy URLs (17,044 accepted). It compares how Python's urllib, urllib3, requests, curl and Node parse each accepted URL, and what they actually send: the Python clients and curl through a local proxy, and all five on their direct path (Node through http.request/https.request; fetch is not covered). There the harness redirects each connection the client opens to a fixture on 127.0.0.1 that records the host and port the client chose, the Host header (http) and the TLS server name from the ClientHello (https), then answers 403 or a fatal TLS alert; every connection goes to 127.0.0.1, so nothing leaves the machine. On the full corpus (Python 3.12.3, urllib3 2.0.7, requests 2.31.0, curl 8.5.0, Node 18.19.1) no client disagrees on scheme, host or port in any of the 15 views, and none reports userinfo in its parse or in an http request. One URL, https://b//yc%80a:;, is refused by urllib3 and requests when sending, so they send nothing. Not observed: DNS (nothing is resolved), whether the certificate is verified, and anything inside TLS; the harness hooks the clients, so it shows what each client chose, not what an unmodified client would do on a real network after DNS.
tests/mutants.py plants 26 plausible bugs one at a time: 15 in the URL check, 8 in the address check and 3 in the Node fetch example. They include the prefix and suffix mistakes, a wrong authority boundary and an IPv4 address read at the wrong offset. 22 break the build (18 in proof files, 4 in build-time examples; some only because a proof script no longer fits the changed code), one is caught by tests/test_addr.py, and the three in the Node example by tests/test_guarded_fetch_node.py.

GitHub Actions runs the audit, the registry check, the tests (with the runner's Node for the WHATWG comparison), a
fixed 1/16 subset of the client comparison and the mutation check on every push to main and on
every pull request. The full client comparison is a local run (python3 tests/compat.py).

Where the name resolves to

The URL check cannot know what an allowed name resolves to. A second command, urlfence addr,
checks resolved addresses against the IANA IPv4 and IPv6 special-purpose registries (as last updated
on 2025-10-09; that the Lean tables match IANA's files is checked by a script, not proven). It decodes
IPv4-mapped addresses, NAT64 addresses in a /96 prefix given with --nat64, and ISATAP
identifiers, and denies 6to4, Teredo and, unless configured, all of 64:ff9b::/96. 2026
advisories in MCP tooling and agent frameworks, among them auth-fetch-mcp (CVE-2026-49857), the MCP
Registry (CVE-2026-44430) and pydantic-ai (CVE-2026-48782), found address checks that missed
internal addresses written in an IPv6 form. The address theorems say that
every address in a registry row that is not globally reachable is denied (IPv4-mapped addresses
instead get the decision of the IPv4 address they carry), and that a denied IPv4 address stays
denied in each of those forms. The address parser is compared with inet_pton on 50,000 strings (for IPv4 its
reading is also proven).

examples/guarded_fetch.py pins by default: on every hop it resolves the host once, refuses if
any answer is denied, and connects only to a checked address, keeping the name for Host and TLS.
A proxy would resolve the name again, so while pinning the example refuses to use one.
examples/guarded_fetch.mjs does the same for Node's http/https.request (not fetch()): it
connects to the checked address on a socket it opens itself, so Node does no lookup of its own.

What it does not do

Unpinned clients: a client that resolves the name itself (a browser, curl, requests) or goes through a proxy is not covered by urlfence addr; pin the connection, or filter egress. The examples pin TCP connections only, not UDP or QUIC, and do not restrict ports.
Some IPv4-in-IPv6 schemes: addresses in unconfigured network-specific NAT64 prefixes, the other RFC 6052 prefix lengths, 6rd, MAP and SIIT-EAM are not decoded, so they are allowed as plain global addresses; deny such prefixes with --deny.
Your own networks: internal services on global addresses must be denied by you.
Redirects: urlfence check decides one URL; re-check every hop, as the examples do.
What the server does: open redirects and proxies on an allowed host are out of scope.
IPv6 and IDNA in URLs: both are refused.

Pair it with egress controls for the connection itself.

Try it

git clone https://github.com/hiroki-abe-58/urlfence && cd urlfence
lake build              # builds the CLI here: .lake/build/bin/urlfence
./scripts/reproduce.sh   # fresh clone of HEAD: build, audit, registry check, tests, client comparison, mutants

It needs git, elan, Python, Node, curl and openssl. To call it from your
own code, examples/guarded_fetch.py (or guarded_fetch.mjs for Node) shows the pattern: check the URL, request exactly the checked
string, check every resolved address and connect only to a checked one, and check every redirect
target before following it.

It is Apache-2.0. I started and lead the project; the code and proofs were written with
Claude Code (Claude Opus 5.5), and so far they have been reviewed only by AI, in separate Claude
sessions. No human has reviewed them yet, so reviews, counterexamples and issues are
welcome. The only guarantees are the theorems; the tests are evidence on the inputs they cover.

References

URLFence repository: https://github.com/hiroki-abe-58/urlfence
Commit described here: https://github.com/hiroki-abe-58/urlfence/tree/ea3c0615aafe2ec9b8360b0d3b14250462e45ae3, with its CI run: https://github.com/hiroki-abe-58/urlfence/actions/runs/40618042270
README, including the limits: https://github.com/hiroki-abe-58/urlfence/blob/ea3c0615aafe2ec9b8360b0d3b14250462e45ae3/README.md
Published theorem statements: https://github.com/hiroki-abe-58/urlfence/blob/ea3c0615aafe2ec9b8360b0d3b14250462e45ae3/scripts/statements.expected
IANA special-purpose address registries: https://www.iana.org/assignments/iana-ipv4-special-registry/ and https://www.iana.org/assignments/iana-ipv6-special-registry/
Advisories cited: CVE-2026-24052, CVE-2026-46341, CVE-2026-33393, CVE-2025-47241, CVE-2026-6322, CVE-2026-49857, CVE-2026-44430, CVE-2026-48782 (GHSA-cg7w-rg45-pc59)

Writing disclosure: this article was drafted and fact-checked with AI assistance under my direction.

PathFence: A Lean 4 Path Checker—and Where Its Guarantees Stop

GeneLab_999 — Tue, 27 Oct 2026 15:02:31 +0000

Correction (2026-10-28). The earlier version of this article described a Workspace API, Windows support, a macOS/BSD fallback, a pure-Python package for Python 3.9+, four explicit openat2 resolve flags, a formal/ directory, a count of 15 theorems and five theorem names, none of which exist, and unsupported microsecond benchmarks. Those claims did not match the repository. This article replaces them with a description checked against code commit e697b4a, with the README packaging clarification in 06753e0. Thanks to the reporter of issue #2. I am responsible for correcting the article published on my account.

PathFence is a Lean 4 library and command-line tool for lexical path-policy decisions. It is not a sandbox or a complete verified file-system implementation.

Repository: https://github.com/hiroki-abe-58/pathfence

What the checker does

A policy has a base directory, allowed roots and denied roots. Roots must already be canonical; /w/.. is refused rather than silently normalized. Requests return allow, deny, or reject.

$ pathfence check --allow /tmp/allowed_dir -- /tmp/allowed_dir_malicious/secret ../x a/../b
{"input":"/tmp/allowed_dir_malicious/secret","decision":"deny","path":"/tmp/allowed_dir_malicious/secret"}
{"input":"../x","decision":"reject","reason":"escapes"}
{"input":"a/../b","decision":"allow","path":"/tmp/allowed_dir/b","root":"/tmp/allowed_dir","rel":"b"}

Empty input and input containing NUL are rejected. Absolute paths are normalized lexically. Relative paths are walked beneath the base: a .. that would leave it is rejected even if later segments would return inside. Containment compares complete segments, so /tmp/ab is not inside /tmp/a. An allowed result names both the allowed root and the relative remainder rel.

These are POSIX lexical rules, not native Windows path rules. Symlinks, mounts, hard links, case folding and concurrent file-system changes are outside the checker’s view.

What Lean proves

The main theorem, check_allow_iff, characterizes exactly when the modeled checker allows a resolved path: it resolves successfully, lies within an allowed root, and lies within no denied root. Other published statements include:

resolve_rel_spec: successful relative resolution agrees with the specified beneath walk.
resolve_rel_within: successful relative resolution remains within the base.
allowedUnder_spec: the reported root is allowed and its remainder reconstructs the resolved path.
parseRoot_render: a root string that parses successfully renders back to exactly that string.
within_iff_render: for a root other than /, segment containment corresponds to equality or a prefix followed by /.

The repository pins 25 published statements. The audit reports 147 theorem declarations, including helpers and generated equation lemmas, at the code revision above. This is not a claim of 147 separate security guarantees. The audit checks dependencies on Lean’s standard axioms, replays library modules through the kernel checker, and pins the published statements and their transitive library definitions by SHA-256. The library imports only Lean’s Init.

The audit itself remains a trust boundary: someone who changes its inputs or implementation can change what it checks. The CLI’s argument parsing, UTF-8 handling and JSON output, the compiler/runtime, Python examples and operating system are not covered by a complete end-to-end proof.

Tests complement the proof

The suite compares the CLI against an independent Python implementation of the documented rules and uses posixpath.normpath for absolute inputs. On Linux it also compares 1,500 generated relative paths against real openat2(RESOLVE_BENEATH | RESOLVE_NO_SYMLINKS) calls on a directory tree without symlinks. Agreement on that tested domain is evidence, not a proof of equivalence to the kernel.

The mutation check plants 11 bugs in the CLI and requires the suite to detect them; three further mutations target the extraction example. GitHub Actions runs build, audit, tests and mutation checks. Tests and review in separate Claude sessions have found issues both around the proven function and in the intended specification, including invalid UTF-8 handling, option-like path arguments, empty inputs and noncanonical roots.

File access still needs kernel enforcement

Do not take an allowed path and assume an ordinary open(path) is safe. A path can be lexically allowed while traversing a symlink into a denied directory.

The repository’s example examples/safe_open.py combines the checker with Linux openat2, opening rel beneath a handle for root. Its signature is:

safe_open(path, allow, deny=(), base=None, flags=os.O_RDONLY, mode=0o644)

This is not a pathfence.Workspace API. The example explicitly passes RESOLVE_BENEATH | RESOLVE_NO_SYMLINKS. Linux’s RESOLVE_NO_SYMLINKS also implies no magic-link traversal; that does not mean the code explicitly passes four flags. The example requires Linux 5.6+ and has no macOS/BSD fallback or native Windows implementation. Trusted root selection and file-system assumptions still matter.

The newer examples/safe_extract.py handles tar/zip archives, accepts only regular files and directories, checks member names, and creates members beneath a new private destination with exclusive creation. It additionally uses RESOLVE_NO_XDEV. Archive links are rejected. Its runtime checks and kernel behavior are separate from the Lean proofs about names; it is not a formally verified archive parser.

There is no Workspace, subworkspace, or atomic_write lifecycle API in this revision. The former article’s microsecond openat2 and fallback benchmarks were unsupported and have been removed. The repository’s actual benchmark concerns the lexical CLI, not those fictional APIs.

Try it

The published pathfence 0.1.0 package is on PyPI and requires Python 3.10+. The 0.1.0 wheels were built from tag v0.1.0 (a959fdc), not from the newer code revision discussed above. They bundle the Lean executable; this is not a pure-Python implementation.

python -m pip install --only-binary=:all: pathfence
pathfence check --allow /tmp/allowed_dir -- ../x a/../b

For the source and verification workflow:

git clone https://github.com/hiroki-abe-58/pathfence
cd pathfence
./scripts/reproduce.sh

The reproduction workflow needs git, elan, Python, sha256sum and Linux 5.6+ for the kernel tests. Its openat2 calls must not be blocked by seccomp; the workflow fails if any test is skipped. Consult the README for current platform support and prerequisites. Package installation alone does not make an agent’s file tools confined.

PathFence is Apache-2.0 licensed and experimental. I started and lead the project; code and proofs were developed with Claude Code (Claude Opus 5.5) and reviewed only by AI, in separate Claude sessions; no human has reviewed them yet. Human review, counterexamples and reproducible issues are welcome.

A Small Attention Fallback Fix Cut Peak Mask-Pass VRAM by 87%

GeneLab_999 — Sat, 24 Oct 2026 08:27:32 +0000

A merged fix in Xiaomi-Lens-0, and why fallback paths deserve their own benchmarks.

When an optional acceleration library is unavailable, what happens next?

In Xiaomi-Lens-0, the pixel mask decoder fell back from flash-attn to nn.MultiheadAttention. In the configuration I tested, that fallback made large images consume enough GPU memory to fail.

An efficient alternative was already implemented. The fix was to make it the fallback.

At a 3-megapixel input size, the additional peak GPU memory used by the mask pass dropped from 18.02 GB to 2.28 GB—about 87%.

The fix has been merged upstream.

The expensive path was the fallback

Xiaomi-Lens-0 can locate and segment objects in images. Its pixel mask decoder includes a PatchSelfAttention module with multiple attention implementations.

Before this change, when the flash-attn path was unavailable, the decoder used its MultiheadAttention implementation.

In the tested execution path, the model’s padding mask caused attention weights to be materialized across all 16 heads. With (P) image patches, the attention matrices scale with (P^2).

That gets expensive quickly as image resolution increases.

The decoder already had a scaled_dot_product_attention implementation, selectable through:

XIAOMI_LENS_DECODER_ATTN=sdpa

It used the same model weights and avoided that memory bottleneck in my test environment.

The opportunity was to make that existing path work automatically for users without flash-attn.

The change

The routing previously looked like this:

if configured_backend == "sdpa":
    return sdpa_attention(...)

if configured_backend == "flash":
    output = try_flash_attention(...)
    if output is not None:
        return output

return mha_attention(...)

After the change:

if configured_backend == "mha":
    return mha_attention(...)

if configured_backend == "flash":
    output = try_flash_attention(...)
    if output is not None:
        return output

return sdpa_attention(...)

These snippets simplify the actual implementation, but capture the change.

Explicit MHA selection remains available. The warning message now reports the correct fallback.

What I measured

The benchmark environment was:

NVIDIA RTX 5090, 32 GB VRAM
Windows 11
PyTorch 2.14.1+cu130
Transformers 5.4.0
No flash-attn installed

I used scikit-image’s coffee photograph, resized to different input sizes, and the README prompt targeting “the coffee cup.”

The benchmark followed the inference stages used by infer.py. The table measures peak GPU memory added by run_forward, the mask pass, above the loaded-model baseline.

It does not measure total application VRAM.

Input size	Patches	Previous MHA fallback	SDPA fallback
0.5 MP	1,944	0.86 GB	0.46 GB
1 MP	3,952	2.58 GB	0.83 GB
2 MP	7,776	8.53 GB	1.55 GB
3 MP	11,616	18.02 GB	2.28 GB

At 3 MP, that is 15.74 GB less additional peak memory for this stage.

In a separate large-image test through a ComfyUI integration, the MHA path ran out of memory while attempting a single 30.75 GiB allocation. The SDPA path completed, with a whole-request peak of 15.05 GB and a runtime of approximately six seconds.

That separate test used a byte-identical copy of PatchSelfAttention, rather than running infer.py itself. Its whole-request measurement should not be directly compared with the mask-pass numbers above.

Did the outputs change?

I compared six image-and-prompt cases, including object segmentation and a reasoning request, checking token IDs, boxes, and every mask logit.

Two checks verified that the routing change behaved as intended:

The new default matched the previous explicit SDPA path bit for bit in all six cases.
Explicitly selecting MHA still matched the previous default bit for bit in all six cases.

Comparing SDPA against MHA:

Generated token IDs and boxes were unchanged.
Masks thresholded at 0.5 had an IoU of 0.9976–0.9998.

There were small differences at mask boundaries. This was a limited six-case comparison, not a comprehensive quality evaluation, but it made the numerical differences visible alongside the memory improvement.

This is not a universal MHA-to-SDPA rule

The result depends on the execution path.

PyTorch’s MultiheadAttention can itself use optimized SDPA, and its documentation recommends need_weights=False to enable that path. SDPA also selects implementations based on the inputs and available backends; calling the API does not guarantee the same memory savings on every device.

Migrating implementations requires care: boolean mask semantics differ between MHA’s key padding mask and SDPA’s attention mask, and SDPA’s dropout must be configured explicitly.

The relevant documentation is here:

The finding in this PR is narrower: this decoder already had an effective SDPA path, and selecting it as the fallback substantially reduced memory use in the measured environment.

Why a small default change matters

An environment variable helps users who know it exists and understand when to set it.

A better fallback reaches users automatically.

This fix changed one file. The work behind it was identifying the expensive execution path, measuring its scaling, checking output differences, and giving maintainers evidence they could review.

For someone whose image previously ran out of memory, that small routing change can determine whether the model is usable at all.

My next step is to investigate a few other models and see whether similar fallback problems recur. If the diagnosis and verification work proves reusable, it could become a shared toolkit.

For now, the practical lesson is simple: benchmark the path your model takes when an optional dependency is missing. That path may deserve more attention than it gets.

From ImportError to Video: Bringing Looking Ahead to Windows

GeneLab_999 — Sat, 24 Oct 2026 04:32:00 +0000

Looking Ahead's 1.3B image-to-video example stopped on my Windows machine before inference started:

ModuleNotFoundError: No module named 'fcntl'

The machine had an RTX 5090. FlashAttention 4 was installed. Neither was enough to get past the import.

My fix, TencentARC/Looking-Ahead PR #2, was merged on October 23, 2026 (UTC). With the patch, the tested 1.3B example produced 80 frames at 768×432 on Windows 11, using PyTorch's scaled dot-product attention fallback.

The change spans six files. The interesting part is how three separate assumptions had to be removed before the fallback actually worked end to end.

Why I wanted to run Looking Ahead

Looking Ahead is a video-generation research project from researchers at Nanjing University, Tencent ARC Lab, and Zhejiang University.

Its method, Future Chunk Prediction (FCP), addresses a shortcut in autoregressive video training: neighboring video chunks can be similar enough that a model relies on local continuity without learning much about how a scene evolves.

FCP adds auxiliary training branches that predict more distant future chunks from the current chunk's intermediate features, without seeing the intervening chunks. Those branches are removed at inference. The authors report improvements in physical consistency; the project page explains the method and shows their comparisons.

The released code includes 1.3B and 5B models. Its documented test environment was Linux with an NVIDIA H200. My contribution makes the tested Windows inference path accessible through the upstream code. It does not change FCP, retrain the model, or establish Windows support for every configuration.

That is why this merge matters to me: the compatibility fix now lives in the research repository, where the next person trying the model can receive it.

1. Installed does not mean importable

The attention modules used is_flash_attn_4_available() before importing flash_attn.cute.

In the tested environment, that availability check reported the installed package. Importing it still failed: its quack dependency imported fcntl, a Unix-specific module unavailable on Windows.

The merged code attempts the import and treats an ImportError as an unavailable optional backend:

FLASH_ATTN_4_AVAILABLE = is_flash_attn_4_available()
if FLASH_ATTN_4_AVAILABLE:
    try:
        import flash_attn.cute
    except ImportError as exc:
        FLASH_ATTN_4_AVAILABLE = False
        warn_flash_attention_fallback(type(exc).__name__, str(exc))

Both attention modules receive this handling. A shared helper logs the selected backend and reports each distinct import failure once.

The warning explicitly says that performance and numerical results may differ. That matters because a run that silently switches backend is harder to reproduce or compare.

The helper receives the exception type and message as strings. It does not cache the exception object and its traceback just to deduplicate a warning.

This check establishes importability, not a guarantee that every subsequent kernel call will work on every device. It also catches ImportError specifically; it does not convert arbitrary runtime failures into silent fallbacks.

2. Cross-attention bypassed the fallback

Getting past the import exposed the next problem.

The code already had an attention() function that selected between FlashAttention 4 and PyTorch SDPA. But cross-attention called the FA4-only flash_attention() directly. Removing FA4 from the environment therefore avoided the import error while leaving an assertion waiting later in the run.

The relevant change is small:

- x = flash_attention(q, k, v, k_lens=context_lens)
+ x = attention(q, k, v, k_lens=context_lens)

Now cross-attention uses the same backend-selection boundary.

There is a semantic condition behind that edit. In the call path covered by the PR, context_lens is None, so the fallback computes full attention. The SDPA branch does not implement arbitrary variable-length padding masks. Routing a masked attention call through it would need additional work.

When FA4 is available, the dispatcher forwards the same arguments to the existing FA4 implementation.

The general lesson is to trace the callers. An optional backend is only optional if the execution paths that need it actually pass through the fallback.

3. Model loading had its own Unix dependency

The remaining fcntl dependency was outside attention.

The project stages base-model files and checkpoints into a local cache, using fcntl for file locking. The default staging path brought the same platform assumption back into the run.

The patch makes the import optional in both loading utilities. If fcntl is unavailable, staging is skipped and the model or checkpoint is loaded from its original path.

This preserves the underlying operation—reading the weights—without pretending that the Unix locking mechanism exists. It also avoids adding a new cross-platform lock implementation for a cache optimization.

On systems where fcntl exists, the existing staging path remains available. On systems where FA4 imports successfully, that attention path remains available too.

What the Windows run established

The PR records the following setup:

Windows 11 and RTX 5090.
Python 3.12 and PyTorch 2.10.0+cu128.
Other package versions from the project's uv.lock.
FCP 1.3B EMA checkpoint, sailboat example, seed 42, and a five-second duration request.

Before the patch, the run stopped at import. With the patch and SDPA, it produced 80 frames at 768×432, with 209 seconds of sampling, 231 seconds for the whole run, and 16.4 GiB peak allocated GPU memory.

One detail belongs beside those results: all reported runs used load_diffusion_pretrained=false. The PR explains that the EMA checkpoint strictly replaces every backbone weight, so the base DiT initialization does not determine the final output. This was not a claim that every model file or loading step could be omitted.

These numbers describe one tested example and environment. They are not an end-to-end validation of training, every checkpoint, or every GPU.

Preserving FA4 and comparing SDPA are different checks

The fallback needed to work, but the original fast path also needed a regression check.

For a controlled experiment, I made FA4 importable using triton-windows and a test-only no-op fcntl module. That shim is not in the PR and is not an installation recommendation—it does not provide real file locking.

With FA4 available, the original branch and the patched branch produced bit-identical decoded frames. That comparison checks whether the patch changed the existing FA4 path.

Comparing SDPA against FA4 answers a different question. On the same example, the first conditioning frame was identical, while frame PSNR was 33.5 dB on average and 31.6 dB at minimum. The generated results were not bit-identical.

FA4 sampling took 154 seconds, versus 209 seconds for SDPA. The fallback made the example runnable with a measurable speed tradeoff. It did not reproduce FA4's exact numerical output.

These are comparisons recorded in the PR's validation notes, not new experiments performed for this article.

The 5B follow-up found the next boundary

I also checked the 5B model with the paper-fan example and documented the result in a follow-up comment.

Sampling completed: 30 latent frames in 231 seconds, with 24.3 GiB peak allocated GPU memory.

The immediately following VAE decode did not fit in the same process on the tested 32 GB GPU / 64 GB RAM machine. The generator and both KV caches remained on the GPU; Windows commit charge passed 104 GiB, and I stopped the run.

Decoding those saved latents separately took 8.2 GiB and 11 seconds. That result points to a phase-lifetime and memory-management problem, beyond the portability fix in this PR.

So the precise outcome is: the 1.3B example completed end to end; the 5B example completed sampling, with decode checked in a separate process. The merge does not include a solution for the combined 5B memory peak.

What I would carry into the next portability fix

This patch connected three things: optional-backend detection, the callers that select that backend, and the platform-specific optimization in model loading.

For another research implementation, I would follow the same checks: attempt the optional import, trace every caller, verify that the fallback preserves the required attention semantics, log the selected path, and test the complete workload. A successful import is only the beginning.

The merged changes are small enough to read alongside the model's setup and inference instructions. FCP and the released models are the research authors' work; my contribution is getting this tested inference path through Windows without replacing the existing FA4 path.

Have you encountered an “optional” dependency that turned out to be mandatory through a different call site?

Drafted with AI assistance from the merged diff, project documentation, and recorded PR validation results. Merge commit: 15f90becc4d37f4f8c74cb0c868b6d855a7c605d.

Same Weights, Same Seed, Different Pixels: Porting PixRestore to ComfyUI

GeneLab_999 — Thu, 22 Oct 2026 09:16:00 +0000

Same weights. Same input images. Same seeds. Two inference paths that each reproduced their own results.

Yet 11.3% of the output's 8-bit channel values differed between them.

That was one result from verifying my unofficial PixRestore integration for ComfyUI. The difference was small—at most 5/255—but enough to make “matches the official output” an incomplete claim.

The useful part of this integration was defining exactly what “matches” meant: which execution mode, which process settings, and which representation of an image.

Here are the problems documented in the implementation and verification runs, and the checks that made the comparison meaningful.

First, define which official run you mean

PixRestore is an image restoration research project. Its released PixRestore-S model restores 512×512 images with one denoiser call, using DINOv2 features as conditioning. My integration exposes it through ComfyUI's usual image inputs and outputs.

The reference environment already required a decision. Upstream pinned PyTorch 2.4.0, but that build did not have the kernels needed for the RTX 5090 used in these tests. The recorded reference therefore used PyTorch 2.14.1+cu130, with the other documented upstream dependency pins.

Then came torch.compile.

Several upstream functions had compile decorators. On the tested Windows environment, the unmodified inference run stopped with TritonMissing at the first compiled call. That left two paths to compare:

Run the official script in eager mode, with TORCHDYNAMO_DISABLE=1.
Add triton-windows to a copy of the reference environment and run the compiled path.

Both ran. They did not produce exactly the same output.

Across the 12 demo inputs, the DINOv2 input, all six recorded DINOv2 feature layers, and the initial noise matched. The diffusion transformer's output differed. The verification report attributes the difference to the Inductor-compiled kernels under bf16 autocast.

The final 8-bit comparison was:

11.3% of channel values differed. This is not the percentage of pixels that looked visibly different.
Maximum absolute difference: 5/255.
Mean absolute difference: 0.11/255.

Two compiled runs matched each other. Three eager runs matched each other.

So a repeatability test could pass for both implementations while an equivalence test between them failed.

The ComfyUI node uses eager execution, removing the compile wrappers from the pinned PixRestore modules. The claim in the README is deliberately specific: it reproduces the official eager path on the tested setup. Compiled execution inside ComfyUI is not part of that claim.

A node inherits the application's numerical settings

A standalone inference script starts in its own process. A custom node runs inside an application that has already configured PyTorch.

In this setup, ComfyUI enabled reduced-precision math reductions for scaled dot-product attention. The official reference process used a different setting. Matching the checkpoint and seed would leave that difference in place.

The integration captures the caller's backend settings, applies the reference settings for its call, and restores the caller's settings afterward. The implementation covers TF32, attention backends, and other precision-related flags.

This excerpt from runtime.py shows the scope:

@contextlib.contextmanager
def official_flags():
    with _LOCK:
        old = _flag_state()
        _apply_flags(OFFICIAL_FLAGS)
        try:
            yield old
        finally:
            _apply_flags(old)

The tests check both sides: the reference settings are active inside the context, and the caller's settings return afterward.

These are process-wide flags. The local lock serializes this pack's use; it does not coordinate every other extension in the process. This is a scoped compatibility measure, not general isolation for arbitrary concurrent PyTorch work.

Random-number state needs similar care. The node seeds the relevant generator inside torch.random.fork_rng, so restoration does not leave ComfyUI's RNG state changed.

The execution environment is part of the comparison, even when it never appears as an argument to the model.

The last conversion is still part of inference

ComfyUI passes images as floating-point tensors. The reference script reads and writes 8-bit images.

That creates another boundary to verify: a float tensor that looks correct must still save to the intended integer values.

The integration follows the reference normalization and output conversion, then returns the resulting 8-bit values to ComfyUI as floats. A small test checks the final round trip for every possible 8-bit value:

u8 = torch.arange(256, dtype=torch.uint8)
image = u8.float() / 255.0
saved = np.clip(255.0 * image.numpy(), 0, 255).astype(np.uint8)
assert (saved == u8.numpy()).all()

This is a shortened version of the repository's image conversion test. It checks the specific conversion path rather than assuming that a float-to-integer round trip is harmless.

For model comparisons, the report also records hashes of the normalized input, noise, DINOv2 features, model output, final float image, and 8-bit result. That makes it possible to locate where a mismatch starts.

Make sure the parity test can fail

The released-weight GPU checks matched the official eager path across 12 demo inputs and four center-crop cases, including execution through ComfyUI's HTTP queue.

But exact matches alone leave a question: is the test actually sensitive to a wrong computation?

The CPU parity tests include two deliberate perturbations:

Change the seed.
Multiply the extracted DINOv2 features by 1.001.

Both must break equality with the reference. The test code makes that expectation explicit.

The real ComfyUI checks also ran an A → B → A sequence with caching disabled and confirmed that the calls executed. An unload-and-reload check verified that the same result survived a fresh model load.

There is an important boundary around the CPU tests: CI uses random weights with the released architecture and fp32 execution. It checks the implementation path, not restoration quality or released-weight GPU parity. The user-facing node still requires CUDA.

I would reuse these checks for another integration: record intermediate values, deliberately perturb an input to the computation, and confirm that a repeatability test is actually rerunning the model.

Exact reproduction does not guarantee a good restoration

Once the integration matched its reference, image quality remained a separate question.

Columns: clean source, degraded input, restoration. Rows: Gaussian noise, blur, JPEG compression. These are 200×200 crops from a synthetic source image, not real-photo restoration results.

The demo contains four synthetic source images with three synthetic degradations each. All 12 cases improved in PSNR against their source images. Noise removal also removed fine texture, and sharpened edges could contain newly synthesized detail.

That is consistent with a generative restoration model: it produces a plausible image, which can differ from the original.

The wrapper's current scope stays narrow: PixRestore-S, one step, CFG 1.0, and 512×512 input. Other sizes are rejected unless the user explicitly selects the official center-crop path. There is no tiling, and the quality of the crop path on real photographs was not evaluated.

Those limits keep the tested behavior identifiable. They also make the next useful experiment clear: evaluate suitable real images before making broader quality claims.

Where the implementation stands

The repository contains Loader, Restore, and Unload nodes, example workflows, and the setup instructions. The measurements and comparisons above come from the October 5 verification runs on Windows 11, an RTX 5090, and ComfyUI v0.38.0; they are not new runs performed for this article.

The lesson I would carry into the next port is to define the reference before chasing exact equality. Pin the code and weights, name the execution mode, compare intermediate tensors, and test the image conversion boundary. Then test output quality as its own problem.

If you have moved a model from a standalone script into a larger application, where did your first numerical mismatch appear: preprocessing, backend settings, or output conversion?

PixRestore research and pretrained models are by the upstream authors. This ComfyUI integration is unofficial. This article was drafted with AI assistance using the repository's source code and recorded verification results.

🛡️ Patched PHP2Shell but php -v Still Says 8.3.6? Here's How to Actually Check

GeneLab_999 — Thu, 22 Oct 2026 05:44:58 +0000

I patched a test box for PHP2Shell, ran php -v, and got... PHP 8.3.6. Same as before. 😅

Turns out that's expected — and if you're judging "are we safe?" by the version number, you can get it wrong in both directions. Here's what I found on Ubuntu 24.04, plus the three checks I now use instead.

TL;DR

PHP fixed CVE-2026-109618 and CVE-2026-109619 ("PHP2Shell", CVSS v4.0 9.2, unauthenticated RCE) in 8.5.12 / 8.4.27 / 8.3.36 / 8.2.35.
On Ubuntu/Debian, the patched package keeps the old upstream version (e.g. 8.3.6). Check the package version and the changelog, not php -v.
Installing the update isn't enough: restart Apache / PHP-FPM, or the old code keeps running.

Quick context: what is PHP2Shell?

Two memory-safety bugs in the PHP runtime itself, disclosed on Oct 21, 2026:

CVE-2026-109618 – "RCE via OOM corruption": an out-of-memory bailout can leave half-initialized request data that cleanup then treats as valid.
CVE-2026-109619 – "RCE via stale global state": request state survives after its memory is freed, and the next request on the same worker uses it.

According to the PHP advisory, every PHP install serving web requests is affected (PHP-FPM, mod_php, php-cgi, FrankenPHP, LiteSpeed), with mod_php at highest risk because an attack can land before your app code even runs. watchTowr reported seeing active exploitation attempts against both.

💡 WordPress folks: this is not a WordPress bug. WordPress.org says no WordPress update is required or planned. You need to update PHP. Security plugins won't help here.

Step 1: Record the "before" state

php -v | head -1
dpkg-query -W -f='${Package} ${Version}\n' php8.3-common

PHP 8.3.6 (cli) (built: Oct  7 2026 18:06:38) (NTS)
php8.3-common 8.3.6-0ubuntu0.24.04.12

Step 2: Install the fix

sudo apt-get update
sudo apt-get install --only-upgrade 'php8.3-*'

Ubuntu's announcement lists 8.3.6-0ubuntu0.24.04.13 as the fixed version for 24.04 (and 8.1.2-1ubuntu2.28 for 22.04).

Step 3: The gotcha 🪤

PHP 8.3.6 (cli) (built: Oct 19 2026 15:16:58) (NTS)
php8.3-common 8.3.6-0ubuntu0.24.04.13

The version string didn't move. Only the build date changed (Oct 7 → Oct 19).

Ubuntu backports security fixes without bumping the upstream number. So:

❌ "8.3.6 < 8.3.36, we're vulnerable!" → wrong, this box is patched.
❌ "We ran apt upgrade, we're fine!" → also wrong if nothing was restarted.

The most convincing evidence is the changelog:

zcat /usr/share/doc/php8.3-common/changelog.Debian.gz | grep -c 'CVE-2026-109618'
# -> 2 on my patched box

The top entry literally references CVE-2026-109618_109619.patch. That one line is what I'd paste into a status update.

Step 4: Restart, or it didn't happen

sudo systemctl restart apache2      # mod_php
sudo systemctl restart php8.3-fpm   # PHP-FPM

Ubuntu's post calls out restarting apache2 for mod_php, and the PHP advisory says to restart every worker. Even if unattended-upgrades installed the fix overnight, the running processes are still the old ones until you restart.

💡 Pro Tip: php -i on the CLI reads /etc/php/8.3/cli/php.ini, not your web SAPI's config. On my box the CLI showed memory_limit => -1. Don't verify web-side mitigations from the CLI.

What about mitigations if you can't patch today?

The PHP advisory lists partial measures: memory_limit=-1 (set so apps can't override it), a lower post_max_size, session.upload_progress.enabled=0 in php.ini or the FPM pool (not via ini_set() or .user.ini), and fatal_error_backtraces=0 on 8.5. It's explicit that these reduce specific attack paths but do not make an installation safe. watchTowr goes further and says .ini-based mitigations should be considered ineffective.

If you're on PHP 8.1 or older, there's no official fixed release. Check your distro or LTS vendor for backports, or upgrade to 8.2+. WordPress.org even suggests taking self-managed old-PHP servers offline until you can update. (And note: 8.2 itself reaches end of life on Dec 31, 2026.)

Results

On my Ubuntu 24.04.5 test box:

Check	Before	After
`php -v`	8.3.6 (Oct 7 build)	8.3.6 (Oct 19 build)
Package version	`…24.04.12`	`…24.04.13`
Changelog mentions CVE	not checked	2
Compare against upstream 8.3.36	"vulnerable"	"vulnerable" ❌ false alarm

Wrapping up

If someone asks "are we safe from PHP2Shell?", answer with three things, not a version number:

Package version + changelog line (the fix is installed)
Restart time of Apache / PHP-FPM (the fix is running)
Logs since Oct 20 reviewed (nobody got in before you patched)

I also wrote a small Python script that compares mixed lists of upstream and Debian/Ubuntu version strings using dpkg's ordering rules (verified against dpkg --compare-versions on 306 pairs). Grab it here: GitHub link

How are you handling version checks across your fleet? Have you hit this backport confusion before? Let me know in the comments! 👇

📝 Japanese versions: Qiita (for non-engineer web managers) / Zenn (engineer deep-dive)
🐦 Follow me on X: @geneLab_999

Sources

Separate Dialogue, Music, and Sound Effects in ComfyUI

GeneLab_999 — Wed, 21 Oct 2026 01:15:47 +0000

A video arrives with one mixed soundtrack. You want to replace the dialogue, but keep the background music and sound effects. Muting the audio removes all three.

I built ComfyUI-DBS to bring that separation into a ComfyUI workflow. It splits a soundtrack into music, sound effects, and speech, then lets you save the parts or combine them again. The repository includes a workflow that writes a new video using the music and effects, with the extracted dialogue saved separately.

It runs locally on a CPU or NVIDIA CUDA GPU. The two available models total about 23 MB to download.

This is an unofficial integration of Dynamic Band Splitting (DBS), by Bingzhe Zhang, Kai Li, and Xiaolin Hu. The research and trained models are theirs; my contribution is the ComfyUI integration, workflows, and verification.

What you can do with the three tracks

DBS produces three audio outputs, often called stems:

Music: the musical part of the soundtrack.
SFX: sound effects.
Speech: spoken dialogue.

For dialogue removal, the workflow adds music + SFX and uses that as the video's new soundtrack. For dubbing preparation or transcription, you can save the speech output on its own. You can also use the separate tracks to adjust their relative levels in a later editing step.

These are estimated sources. Some dialogue can remain in the other tracks, and some wanted sounds can be affected. Start with a short excerpt and listen to every output before processing a longer video.

A 12-second excerpt from Tears of Steel and the DBS-TIGER stems produced by this integration on CPU. Source film: Blender Foundation, CC BY 3.0. The excerpt comes from the DBS project page.

The spectrogram shows the outputs, but listening is the useful test. The authors provide audio examples and a listening demo for exploring the underlying model. Those examples are separate from the ComfyUI integration.

Install ComfyUI-DBS

You need ComfyUI v0.38.0 or later, with the V3 node API, and Python 3.10 or later. A CUDA GPU is optional.

Run these commands from your ComfyUI root directory, using the Python environment that runs ComfyUI:

git clone https://github.com/hiroki-abe-58/ComfyUI-DBS custom_nodes/ComfyUI-DBS
python -m pip install -r custom_nodes/ComfyUI-DBS/requirements.txt

If you use a portable installation, replace python with that installation's Python executable. Installing dependencies into a different Python environment will not make them available to ComfyUI.

Download the two models:

python custom_nodes/ComfyUI-DBS/tools/download_model.py --models-dir models/dbs

The download script uses pinned model revisions and checks the files' SHA-256 hashes. It creates these folders:

ComfyUI/
  models/
    dbs/
      DBS-TIGER-DnR/
      DBS-BSRNN-DnR/

The requirements are einops and safetensors, which ComfyUI usually already includes. After setup, the nodes load local model files; they do not download models during a run.

Restart ComfyUI to load the new nodes.

Separate the dialogue from a video

Open the supplied video_remove_dialogue.json workflow from:

custom_nodes/ComfyUI-DBS/workflows/gui/video_remove_dialogue.json

Choose your video in Load Video. The workflow's clip.mp4 filename is a placeholder for your own file.

The workflow performs these steps:

Load Video → Get Video Components extracts the frames, frame rate, and audio.
DBS Loader → DBS Separate separates the audio into music, SFX, and speech.
Merge Audio, set to add, combines the music and SFX.
Create Video → Save Video writes a video with that combined soundtrack.
A separate audio output saves the dialogue as FLAC.

The supplied workflow uses channels = each channel to process the stereo channels independently, and output_sample_rate = input to return audio at the input sample rate. The model itself works at 44.1 kHz; the node handles resampling.

For an audio-only input, the GUI workflow folder also includes:

separate_soundtrack.json: saves all three stems as FLAC.
remove_dialogue.json: saves music + SFX, plus the separate dialogue track.

You can begin with these workflows and connect the audio outputs to your existing graph.

Which model should you choose?

DBS-TIGER-DnR is the default. It has 1.0 million parameters and higher reported separation scores than DBS-BSRNN on the authors' DnR v2 evaluation.

DBS-BSRNN-DnR has 4.7 million parameters, but it was faster in the repository's local measurements. It is the practical starting point for CPU use.

Here are two examples from the recorded verification runs:

On an RTX 5090, a 10-minute input processed as a channel mean took 37.9 seconds with DBS-TIGER and 26.9 seconds with DBS-BSRNN.
On an Intel Core Ultra 9 285K using 24 CPU threads, a 60-second input processed as a channel mean took 122.5 seconds with DBS-TIGER and 32.8 seconds with DBS-BSRNN.

These measurements used Windows 11, an already-loaded model, and the pack's runtime in-process. They exclude model loading and video export. They are useful reference points, not speed promises for another machine.

Stereo takes more work because each channel is processed separately. For the same 10-minute input on the RTX 5090, the recorded stereo times were 74.5 seconds for DBS-TIGER and 53.7 seconds for DBS-BSRNN. Use those figures when considering the stereo video workflow above.

With the loader set to auto, the pack uses ComfyUI's GPU when it is CUDA and otherwise falls back to CPU. Apple and AMD GPU acceleration are not implemented in this pack.

What I verified—and what still needs listening

A model integration can load successfully while changing the model's behavior. I wanted to check the audio output against the official package as well as make the nodes work.

The verification report records:

Six CPU comparison cases: the pack's raw output matched the official package byte for byte.
Four CUDA comparison cases: outputs matched byte for byte when both sides used the documented deterministic PyTorch settings. Default CUDA runs can differ slightly, including between runs of the official code itself.
Real ComfyUI queue checks: audio separation, music-plus-SFX output, and video export were exercised through ComfyUI, alongside a clean-install check.

Those checks establish integration fidelity under the tested conditions. They do not establish perfect separation quality, or byte-identical output for every exported file and configuration. The report documents the export rounding and CUDA differences too.

The released models were trained on DnR v2, which combines English speech, music, and sound effects into film-like mixtures. Songs with sung vocals, other languages, or unusually loud music need their own evaluation. Singing may be assigned to the music track.

For a first test, choose a short clip with clearly audible dialogue, music, and effects. Listen to the original, the extracted speech, and the recombined music + SFX. That will tell you much more about your use case than a spectrogram alone.

Try ComfyUI-DBS and the included workflows on GitHub. If it is useful in your workflow, a star helps other ComfyUI users discover it. Feedback with your model choice, device, and the kind of audio you tried is welcome in the repository's issues.

ComfyUI-DBS is independent of the DBS authors and Comfy Org. The integration code is MIT-licensed; the vendored DBS code and model licensing are documented in the repository's license notes.

Decision models are English-first. I measured them in Japanese, then built one.

GeneLab_999 — Thu, 01 Oct 2026 02:21:03 +0000

What happens to System One decision models outside English: a position prior in Laya, an open Japanese model, a translated benchmark, and what transfers back to English.

Decision models had a big September. TypeSafe AI shipped Jev and called it the first "System One" model. Liquid AI followed with d1. Open implementations appeared within days: Laya, AnyJev, kev, Lev.

The idea is simple and good. Instead of asking an LLM to write JSON and parsing it, you send text plus typed questions and get back probabilities, with zero output tokens:

noul: yes / no, returns P(yes)
choice: pick one of named options, returns a distribution
score: a position on an ordered scale, returns an expected level and a distribution

Almost every public number for these models is in English. I work with Japanese text, so I measured them in Japanese. This post is what I found, what I built, and what I'd tell anyone building one for another language.

TL;DR

laya-multilingual never picked the first level of an ordinal question in Japanese: 0 of 300. Same in English: 0 of 290. A label-free check for this is now in Laya.
I built sokudan, an open 310M Japanese decision model. On 300 Japanese business messages: choice accuracy 0.880, score RPS 0.075, bool AUROC 0.844. pip install sokudan, runs on CPU, CUDA or Apple Silicon (MLX).
Trained only on Japanese, its choice transfers to English almost intact; its yes / no does not.
I published a Japanese translation of LocalLLaMA's typed-decisions benchmark, with every case back-translation-checked.

1. The first thing I found: a position prior

I wrote 300 synthetic Japanese support messages (bench_ja) with three unseen schemas: route to one of four departments, rate urgency on three levels, flag churn intent. Then I ran laya-multilingual on them.

Choice was fine. Score was not: its RPS was 0.232, worse than always predicting the majority class (0.197). Looking at the predictions, it had chosen the first-listed urgency level 0 times out of 300, while that level was the correct answer for a real share of the messages.

The test that made this undeniable is simple and needs no labels. Give every option the same text:

level 0: a request
level 1: a request
level 2: a request

A model that reads content, not position, should spread its probability evenly. Any preference is pure presentation. Measure slot 0's log-probability against the mean over slots, and the first-slot rate over all orderings of three real options (1/3 if order doesn't matter).

I reported it (laya#131), and the maintainer documented it in the README and model card. Then I upstreamed the check itself:

laya#259 (merged): presentation_checks.py, the identical-option control, first-slot rate and a parity check, so any retrained checkpoint can be tested for the prior.
laya#650 (merged, ships in 0.3.22): fixed states in Japanese, Korean, Hindi and Turkish. The first-slot check fails in all four.
laya#753 (open): the same control for choice. Here laya-multilingual favours slot 0 in all five languages. So the avoidance isn't a general dislike of the first option; it's specific to ordinal questions.

I ran the same control on kev and Lev. On score questions, both put less probability on slot 0 than on the other slots when every level carries the same text. For Lev, averaging the score over the presented order and its reverse raises score accuracy by 6.9 points on the English bench (8.7 on the Japanese one) and brings the control close to zero (lev#2, open, off by default).

Lesson 1: accuracy alone won't show you this. Measure presentation with a label-free control, in every language you ship.

2. Building a Japanese one

sokudan (即断, "snap decision") is my answer to "what if the decision model were built for Japanese from the start".

Backbone: sbintuitions/modernbert-ja-310m (MIT). 314.6M parameters.
State and question are encoded jointly in one sequence, with a marker token per option; a small head reads each marker. Score uses a cumulative-link head, since the number of levels is decided per request.
Training data: synthetic, 21 domains, 4,833 documents, 31,243 labelled (document, question) pairs. One RTX 5090.
Apache-2.0. Weights on Hugging Face. pip install sokudan.

On the same 300 Japanese messages, with Lev measured on the same machine:

bench_ja (300)	choice acc	score RPS ↓	score acc	bool acc	bool AUROC
sokudan v0.2 (310M)	0.880	0.075	0.817	0.780	0.844
Lev (calibrated)	0.887	0.138	0.643	0.817	0.889
laya-multilingual	0.747	0.232	—	0.543	0.523
majority class	0.380	0.197	—	0.703	—

The honest reading: Lev, a much larger model (about 9 GB of VRAM in bf16 in my runs) trained for English, is as good or better than my Japanese one on choice and yes / no. Scale buys a lot of transfer. Where the dedicated model wins is the ordinal question, which is exactly where the position prior hurts. sokudan's own cost is small: about 24 ms per bench item on an RTX 5090, 1.3 GB of VRAM, and it runs on a CPU.

import sokudan

agent = sokudan.load("GeneLab/sokudan-ja-310m")
result = agent.predict(
    "先月の請求で同じ金額が二回引き落とされています。至急ご確認ください。",
    {"department": {"type": "choice",
                    "instructions": "この問い合わせはどの部署が担当すべきか",
                    "criteria": {"請求": "支払い・返金", "技術": "不具合・障害",
                                 "営業": "料金・新規契約", "その他": "上記以外"}}},
)
print(result["answers"]["department"]["choice"])  # 請求

There's also a server that speaks the same /v1/systemone request and response shape as TypeSafe's public API reference (and Liquid's d1 uses the same shape), so a client written for that format can point at localhost.

3. What transfers back to English

I trained sokudan on Japanese only, then ran it on the English version of the bench (290 messages):

	English	Japanese
choice acc	0.872	0.880
score RPS ↓	0.114	0.075
bool acc	0.690 (majority 0.683)	0.780

Choice carries over almost untouched. Score degrades but stays useful. Yes / no collapses to the majority class. My reading: choosing between named options leans on matching the option text against the state, which a mostly-Japanese backbone can still do in English; a calibrated yes / no needs the model to have learned what "yes" looks like in that language.

So: sokudan is a Japanese model. Please don't use it for English yes / no questions.

Lesson 2: if you're building for a non-English language, report the transfer table both ways. Which question types survive the language shift is not obvious, and it isn't the same for all three.

4. A Japanese typed-decisions benchmark

My bench is one family of synthetic support messages. To test outside it, I translated LocalLLaMA's typed-decisions (Apache-2.0) into Japanese: 1,600 cases across agent traces, customer service, invoices and security incidents.

Machine translation needs checking, so every case was back-translated and judged against the source by a second model. Overall match: 0.946. Every case carries its match flag, so you can filter. Dataset: GeneLab/typed-decisions-ja.

Zero-shot on the 400 test cases, same scorer for both languages:

	Japanese	English
Lev	0.628	0.635
Qwen3-8B via AnyJev	0.625	0.648
label prior	0.483	0.483
sokudan	0.424	0.435
laya	0.348	0.353

Two things. Every model loses at most 0.023 going from English to Japanese, which is decent evidence the translation kept the difficulty. And sokudan is below the label prior here: agent traces and invoices are a different world from the business messages it was trained on. A small dedicated model is dedicated.

5. Things that bit me

Option descriptions matter enormously. On the department question, giving each option a short description versus bare labels: choice accuracy 0.880 vs 0.537. Short labels like "billing" or "technical" only mean something once described.

Catch-all options are under-chosen. When "Other" is the right answer, sokudan picked it for 11 of 38 cases, though P(Other) still ranks those cases well. Threshold P(Other) instead of taking the argmax. I later found part of the cause in my own training data: 904 rows had a "none of these" option, and it was never the correct answer. The model learned exactly that.

Three seeds lie. My first release reported a three-seed mean. Score accuracy across those seeds was 0.663, 0.800 and 0.827; the mean described no actual run, and the shipped weights were the 0.663 one. I moved to 16 seeds per condition, exact permutation tests, and decision rules committed before training. Most ideas I tested afterwards failed that bar. The one that passed was the simplest: v0.2 is a uniform average of eight seeds' weights.

The same fix works on one model and not another. Order averaging lifts Lev's score accuracy by 6.9 points. On sokudan I tried three versions of it (at inference, as a training penalty, and by shuffling options in the data); each moved some position checks, but none kept accuracy. Measure the fix on your model; don't import it.

If you're building one for your language

Write a small bench in your language with schemas the model has never seen, and keep it out of training.
Run the identical-option control and the first-slot rate per question type. Laya's presentation_checks.py already has fixed states for five languages; adding yours is a few lines.
Report the transfer table to and from English.
Use enough seeds to see the spread before you believe a difference.
Check your training data for options that are always wrong.

Links

sokudan: GitHub · Hugging Face · PyPI · Colab
Benchmarks: bench_ja / bench_en in the repo (CC BY 4.0, evaluation only) · typed-decisions-ja
Listed in the Jev Decision Index

sokudan is an independent open-source project, not affiliated with TypeSafe AI or Liquid AI. "System One" is TypeSafe AI's name for this category. TypeSafe's terms prohibit using its service or outputs to build similar products, so I have never called Jev, and none of the numbers above are Jev's. I haven't measured d1 either.

I didn't fix the bug: contributing to a 20k-star ML repo by measuring it

GeneLab_999 — Thu, 24 Sep 2026 04:41:45 +0000

Last week I opened an issue on laya, an open-source decision model with a little over 20k stars. The issue reported that one of its checkpoints almost never picks the first-listed option on ordinal questions. About 36 hours later, three things had happened. The maintainer had documented the limitation in a release. He had asked me to run the before/after on the retrained checkpoint. And he had merged a regression check I wrote. That was four days after my first measurement.

Nothing is fixed. The fix is a retrain, and the retrain hasn't happened yet. What I contributed is narrower. I think it is also the kind of thing an outsider is best placed to contribute: a measurement nobody could wave away, and a tool that says whether the fix worked.

The fastest way I've found to contribute to an ML repo you don't maintain: measure it, make the measurement impossible to explain away, and then hand the maintainer a tool.

The timeline, in UTC:

Sep 20 — first Japanese baseline run
Sep 22, 05:56 — issue #131 opened
Sep 22, 06:40 — condition F posted (position vs. label, explained below)
Sep 22, 07:15 — a third party, AlKor13, traces it to the weights
Sep 22, 10:56 — my labelled A/B test of his hypothesis
Sep 22, 20:40 — the maintainer's decision
Sep 23, 07:25 — v0.3.7 ships with the limitation in the README
Sep 23, 14:42 — PR #259 opened
Sep 23, 17:48 — PR #259 merged

What laya is, and why I was measuring it

laya is a non-autoregressive "System 1" decision model. You give it some text and a set of typed questions: choice, score for ordinal levels, and noul for yes/no. It answers all of them in one forward pass, with probabilities and no text generation. It ships several checkpoints, including an English laya and a laya-multilingual.

I'm building a Japanese model in the same space (sokudan). Before writing any training code, I wanted a baseline: how well does the existing multilingual checkpoint handle Japanese?

I built 300 label-conditioned Japanese business emails. The labels were fixed first. Then a local LLM wrote an email to match them, and any email containing the label words themselves was thrown out and regenerated. Each email got three questions: department (4-way choice), urgency (3-level score) and whether the customer is hinting at cancelling (bool).

The results split by question type. choice worked: 0.747 accuracy against a 0.380 majority-class baseline. score lost to the majority baseline (RPS 0.232 vs 0.197, lower is better). bool also lost to the majority baseline (0.543 vs 0.703), with an AUROC of 0.523. That is barely better than ranking at random.

One comparison I did not run is TypeSafe's Jev, the hosted API laya benchmarks itself against. Its customer agreement prohibits using the service or its outputs to develop similar products, and my project is a similar product.

The number that didn't fit

"Worse than majority" is a finding, not an explanation. The confusion matrix for score was more interesting. The lowest level, "not urgent", was never predicted in all 300 emails, even though 77 emails had it as the gold label.

At least three explanations fit that. The ordinal head could be degenerate. The model could be reading position rather than content. Or this particular Japanese phrase could be the problem.

To separate them, I re-ran the same 300 emails under five option schemas: original order, reversed, reworded (low / medium / high), reworded and reversed, and four levels. In all five, the first-listed option was chosen 0 or 1 time out of 300.

The cleanest pair was the original order against the reversed one. "Not urgent" was chosen 0 times when listed first and 250 times when listed last. The emails were the same, the words were the same, and only the slot had changed.

Making it hard to explain away

Before reporting, I tried to list the replies a busy maintainer could reasonably give, and to answer each one with data before he had to ask.

"Your harness is wrong." I re-ran the benchmark using only the two lines from the README, laya.load() and agent.predict(), with no wrapper of mine in between. Then I compared the results to my saved probabilities. The maximum difference was 0.0 after the probability floor I apply, and 2.2e-16 on the raw values.

"It's a Japanese problem." I built 290 English emails with the same label weights, the same generator and the same rejection rules, and ran the same five conditions. The multilingual checkpoint went 0 for 290 in every one of them. English is one of its training languages, so "it can't read the input" doesn't explain this.

First-listed option chosen, per condition (original / reversed / reworded / reworded reversed / four levels):

checkpoint	Japanese (n=300)	English (n=290)
`laya-multilingual`	0, 0, 1, 1, 0	0, 0, 0, 0, 0
`laya` (English)	13, 56, 8, 1, 110	65, 74, 0, 5, 4

The English checkpoint picks the first slot in most conditions, on the same data through the same harness. So the task isn't the cause, and neither is the harness. It comes down to one checkpoint. I opened #131 with a title that said exactly that.

(A correction to myself: in the issue I summarised the English checkpoint as picking the first option "22–26% of the time". That holds for the two original orderings. It is 0 in one condition and under 2% in two others. The table above is the honest version.)

"Is it the position or the word?" Within any single fixed ordering, "the model rejects slot 1" and "the model rejects whichever word sits in slot 1" predict the same table. Someone on X asked whether the effect survives shuffling. Twenty-two minutes later I had condition F: the option order is shuffled per item, with a fixed seed. The results:

The first slot was chosen 0 times out of 300.
Choices by slot were [0, 149, 151].
Choices by label were 75 / 93 / 132.
Each label had sat in the first slot 90 / 109 / 101 times.

So every label lost exactly the picks it had while it was in slot 1. Slots 2 and 3 split evenly, so this isn't a preference for the last slot either. One run was enough to separate position from label.

Someone else went deeper

What happened next was the best part, and it wasn't my work. AlKor13, who is not a maintainer, read the raw marker logits straight off the forward pass, before temperature and softmax.

On the identical code path, swapping only the checkpoint made the hole appear or disappear. Then he ran the control I wish I'd thought of: three identical options, so the inputs differ only by position. The English checkpoint came out essentially flat. The multilingual one came out sharply position-dependent. That settled it: the cause is in the weights, not the code.

He went one step further. Score options are rendered with a level N: prefix, and dropping that prefix made the slot-0 suppression vanish from the raw logits. But he stated the limit of his own result. Without the prefix the input is off-distribution, so the recovery might just be the learned prior getting scrambled. Settling that would take labelled data.

Testing someone else's hypothesis, and my own

I had the labelled data, so I ran three renderings on both benchmarks: A is the shipped level N: rendering, C drops the prefix, and D uses word ordinals. My harness reproduced agent.predict() to within 4.6e-5 under condition A. I compared the renderings with paired McNemar tests on identical items:

bench	change	score accuracy	items that flipped correctness	p
ja	A → C	0.447 → 0.513	56.7%	0.145
ja	A → D	0.447 → 0.570	38.3%	0.0007
en	A → C	0.266 → 0.428	56.9%	0.0003
en	A → D	0.266 → 0.293	19.3%	0.350

Two of the four comparisons are significant, and they are different conditions in different languages. D wins in Japanese and C wins in English, and each is null in the other language. The claim this supports is "the shipped rendering isn't the best one for this checkpoint". It does not support "drop the prefix and it's fixed".

I'll admit the accuracy column alone had me halfway to writing the second claim. The paired test is what stopped me, and I said so in the thread.

The column that matters is the flip rate. Under C, 57% of items change correctness, while headline accuracy moves by 6.7 to 16.2 points. A cosmetic change to the option string nearly re-rolls the prediction. That is an instability, not a mitigation. As a control, removing the prefix makes the English checkpoint worse on the English set (0.583 → 0.500). So level N: isn't harmful in general. The multilingual checkpoint has learned something wrong about that specific pattern.

The maintainer's call

About fifteen hours after I opened the issue, the maintainer, NandhaKishorM, replied to both of us. He called the thread "a model of how to run a bug down" and made three decisions:

The bug is in the weights, not the code.
He would not ship a new default rendering. He cited the 57% flip rate: changing the rendering would swap one instability for another.
The real fix is in training. Ordinal options need the same position balancing that choice options already get.

The next morning, v0.3.7 shipped with a line in the README's limits section. It says laya-multilingual has a position bias on score questions, that English score questions should go to the English checkpoint, and that users should validate score outputs on their own data for other languages. The issue stays open until a retrained checkpoint lands.

I offered to run the same A–F and A/C/D before/after on that checkpoint. He said he'd ping me when it's ready.

Handing over a tool

That offer had a weak point: it depended on me. My benchmarks are CC BY 4.0, so anyone can rerun them. But the question the retrain has to answer doesn't need labels at all: did the slot prior go away? So I wrote PR #259:

python research/eval/presentation_checks.py --model <retrained checkpoint> [--subfolder multilingual]

It uses ten short English support messages that are fixed in the file, with no dataset and no labels. It runs two checks:

score_slot0_identical is AlKor13's identical-option control turned into a gate. It measures slot 0's raw logit minus the slot mean, over K = 3, 4 and 5 identical levels, and requires the result to be at least −0.20.
score_first_slot_permuted puts the three real levels in all six orders for each message, so every level sits in every slot exactly twice. A model whose answer doesn't depend on order picks the first slot in exactly 1/3 of decisions. The gate is at least 0.15.

Results on the checkpoints that ship today:

checkpoint	slot-0 logit (gate ≥ −0.20)	first-slot rate (gate ≥ 0.15)	verdict
`laya` (English)	+0.664	0.217	PASS
`laya-multilingual`	−0.492	0.017	FAIL

I fixed the threshold conditions before the real 10-message run, and I didn't move them afterwards. There were two conditions. First, in every leave-one-out subset, multilingual must fail and English must pass. Second, each checkpoint's worst leave-one-out value must clear its gate by at least 0.10 logit (slot 0) or 0.05 (first-slot rate). The tightest margin turned out to be the English first-slot rate, at 0.054.

The gate is one-sided on purpose. With identical options, the English checkpoint isn't flat either. It leans toward early slots, and the lean grows with K. A two-sided "no position effect" gate would fail the checkpoint everyone agrees is fine. So the gate asks only the narrower question #131 is about: is slot 0 suppressed?

The harness checks itself before it gives a verdict. It first compares its logit path against Agent.system_one on every message. On the shipped checkpoints, the maximum |Δp| was 4.98e-5, which is just the API's 4-decimal rounding. If the difference exceeds 1e-3, the script exits with code 2 and reports no verdict. Exit 0 means pass, 1 means a check failed, and 2 means the harness disagrees with the package. There are 69 offline tests using scripted logits. For example, a scripted slot-0 hole fails both checks, and an order-invariant model scores exactly 1/3.

The PR also lists its own limits. Passing is not accuracy. The check covers English only, score only and ten short messages. And the thresholds were set on CPU with fp32.

Before opening the PR

I spent more time reading the repo than writing the script. Tests there are plain scripts, not pytest. CI doesn't load model checkpoints. Research code lives under research/. A new test has to be registered in both ci.yml and release.yml, and an open PR, #184, hadn't yet settled how research tests get wired in. So I didn't wire mine in. I said so in the PR and offered to do it once #184 lands. Nothing under laya/ changed, and I added no new dependencies.

The same afternoon, another contributor, Rukafuu, had proposed a general metamorphic robustness framework in #244, and the maintainer had invited them to start with option permutation. That was their work to do. I kept my check specific to #131 and noted that it could move into their framework once it exists. Their PR, #269, has since been merged.

259 was merged about three hours after I opened it. The maintainer said a label-free check answering one question was "exactly what #131 needs". He also said that separating a failed check from a harness disagreement in the exit codes made it "easy to trust". That second point is the one I'm proudest of, because it's the part nobody asked for.

On using Claude Code

I used Claude Code throughout: for the harness, the offline tests and drafting the PR text. The commit carries a Co-Authored-By line. The decisions about what to measure, what to claim, what to take back and where to stop were mine, and so are any mistakes.

What I'd tell myself next time

Measure before you report, and check your harness against the official package before you measure anything that matters. "Your harness is wrong" is the cheapest possible dismissal. Rule it out first.
Answer the obvious objections before anyone raises them. Is it the language? Run it in English. The harness? Check parity. The word? Shuffle per item. Each of those came back as one line in the thread instead of a round-trip.
Take back your own overclaims, out loud. McNemar turned my "the prefix is the problem" into "the rendering is unstable". The weaker claim is the one the maintainer could act on.
Credit precisely. The most important control in this story came from AlKor13. My PR is his idea turned into a gate, and the PR says so.
Don't take work someone else was just handed. #244 was Rukafuu's. Keeping my check narrow cost nothing and avoided stepping on them.
Don't claim the fix. I found it, reported it, and merged the tool that will say whether the retrain worked. That's the whole claim.

Where it stands

131 is open, and the retrain is pending. When it lands, `presentation_checks.py` gives the first answer, and I'll run the labelled A–F and A/C/D before/after on top of it.

What I posted the day it merged:

// Detect dark theme var iframe = document.getElementById('tweet-2102969840386687112-803'); if (document.body.className.includes('dark-theme')) { iframe.src = "https://platform.twitter.com/embed/Tweet.html?id=2102969840386687112&theme=dark" }

Repo: https://github.com/NandhaKishorM/laya
Issue #131: https://github.com/NandhaKishorM/laya/issues/131
PR #259: https://github.com/NandhaKishorM/laya/pull/259
Related: #171, #244
My data and repro scripts: baseline_ja.md, baseline_en.md

Claude Opus 5.5 vs GPT-6 Astra vs GPT-6 Sol: the effort knob matters more than the model

GeneLab_999 — Wed, 23 Sep 2026 11:27:37 +0000

On September 22, 2026, Anthropic shipped Claude Opus 5.5 and OpenAI shipped GPT-6 Sol on the same day. OpenAI's flagship, GPT-6 Astra, had landed three weeks earlier.

If you tried to pick one from the launch posts, you probably noticed the problem: nobody compared against the right opponent. Anthropic's table compares Opus 5.5 with GPT-6 Astra and the previous GPT-5.6 Sol. OpenAI's Sol post compares with Claude Opus 5 and Fable 5.1, not Opus 5.5. Every chart is technically true and none of them answers "which one should I call from my code today?"

So I went to Artificial Analysis (AA), which ran all three through the same ten evaluations at every reasoning-effort level, and did the cost math.

TL;DR

Raw intelligence: Opus 5.5 (max) scores 58 on AA's Intelligence Index. Astra (max) scores 53, Sol (max) 48.
List price: Sol is cheapest per token, Astra is 2.5x Opus 5.5.
Per-task cost flips the ranking: at max effort Opus 5.5 emits ~4x more output tokens than Astra, so Opus max ($5.98/task) costs more than Astra max ($3.26/task).
The useful finding: below ~$1.30 per task, Sol and Astra trade the lead. Above ~$1.30, Opus 5.5 is on top at every budget. Opus 5.5 at high ($1.82) outscores Astra at max ($3.26).
The effort setting moves your bill more than the model choice does.

1. The price sheet (and its fine print)

Per 1M tokens, standard tier, as of September 23, 2026:

	GPT-6 Sol	GPT-6 Astra	Claude Opus 5.5
Input	$2.00	$10.00	$4.00
Output	$10.00	$50.00	$20.00
Cache read	$0.20	$1.00	$0.20
Cache write	$2.50	$12.50	$5.00 (5 min) / $8.00 (1 h)
Prompt > 272K input tokens	2x input & cache, 1.5x output, whole request	same as Sol	no surcharge up to 1M

Two things developers tend to miss:

Sol and Opus 5.5 have the same cache-read price. Anthropic says cache reads make up the majority of agentic and coding costs. The more your agent re-reads a cached prefix, the less the 2x headline gap matters.
OpenAI's long-context surcharge applies to the entire request, not just the tokens past 272K. For a cache-heavy, long-context agent, Opus 5.5 can end up cheaper than Sol per request.

Also: tokenizers differ between vendors (Anthropic itself notes its newer tokenizer produces roughly 30% more tokens for the same text than its older one). Per-token prices are not a common currency. Compare cost per task instead.

2. Tokens per task is the hidden multiplier

At max effort on AA's suite, Opus 5.5 emits ~119k output tokens per task. Astra emits ~27k, Sol ~31k. That's why Astra, at 2.5x Opus's per-token price, still comes out cheaper per task at the top settings.

Here's the full grid from AA (Intelligence Index score / estimated USD per task):

effort	GPT-6 Sol	GPT-6 Astra	Claude Opus 5.5
low	34 / $0.13	46 / $0.82	42 / $0.55
medium	40 / $0.25	50 / $1.54	51 / $1.34
high	43 / $0.37	51 / $1.73	54 / $1.82
xhigh	44 / $0.53	52 / $2.31	56 / $3.46
max	48 / $1.06	53 / $3.26	58 / $5.98

Note that Opus 5.5 is cheaper than Astra at low and medium, roughly equal at high, and more expensive at xhigh and max.

3. Buy intelligence by the dollar

The question I actually care about: for a given per-task budget, which (model, effort) pair gives the highest score? That's a tiny script:

# Artificial Analysis Intelligence Index v4.3.2 (Sept 22, 2026): (score, est. USD per task)
AA = {
    ("gpt-6-sol", "low"): (34, 0.13),     ("gpt-6-sol", "medium"): (40, 0.25),
    ("gpt-6-sol", "high"): (43, 0.37),    ("gpt-6-sol", "xhigh"): (44, 0.53),
    ("gpt-6-sol", "max"): (48, 1.06),
    ("gpt-6-astra", "low"): (46, 0.82),   ("gpt-6-astra", "medium"): (50, 1.54),
    ("gpt-6-astra", "high"): (51, 1.73),  ("gpt-6-astra", "xhigh"): (52, 2.31),
    ("gpt-6-astra", "max"): (53, 3.26),
    ("claude-opus-5-5", "low"): (42, 0.55),    ("claude-opus-5-5", "medium"): (51, 1.34),
    ("claude-opus-5-5", "high"): (54, 1.82),   ("claude-opus-5-5", "xhigh"): (56, 3.46),
    ("claude-opus-5-5", "max"): (58, 5.98),
}

def best_under(budget_usd: float):
    """Highest-scoring (model, effort) whose estimated cost fits the per-task budget."""
    affordable = [(score, -cost, cfg) for cfg, (score, cost) in AA.items() if cost <= budget_usd]
    if not affordable:
        return None
    score, neg_cost, cfg = max(affordable)  # ties go to the cheaper config
    return cfg, score, -neg_cost

for budget in (0.25, 0.60, 0.90, 1.10, 1.40, 2.00, 4.00, 6.00):
    print(f"${budget:.2f} ->", best_under(budget))

Output:

$0.25 -> (('gpt-6-sol', 'medium'), 40, 0.25)
$0.60 -> (('gpt-6-sol', 'xhigh'), 44, 0.53)
$0.90 -> (('gpt-6-astra', 'low'), 46, 0.82)
$1.10 -> (('gpt-6-sol', 'max'), 48, 1.06)
$1.40 -> (('claude-opus-5-5', 'medium'), 51, 1.34)
$2.00 -> (('claude-opus-5-5', 'high'), 54, 1.82)
$4.00 -> (('claude-opus-5-5', 'xhigh'), 56, 3.46)
$6.00 -> (('claude-opus-5-5', 'max'), 58, 5.98)

Plotted as "best score you can buy at each budget":

Under ~$1.30/task: Sol owns most of the range. Astra low wins a narrow band around $0.82–$1.05.
Over ~$1.30/task: Opus 5.5 leads everywhere (it ties Astra once, briefly, at score 51).
Sol tops out at 48 and Astra at 53. Past those points, paying more buys nothing.

At 10,000 tasks a month, this stops being academic:

Opus 5.5 high scores one point above Astra max and costs $14,400/month less in this illustration. Also note the gap between Opus 5.5 medium and max: about 4.5x the cost for 7 more points.

4. Benchmarks have referees

Anthropic's launch table shows Opus 5.5 at 66.4% on Terminal-Bench 4.0 vs Astra at 57.9%. The footnotes matter: Opus ran at xhigh in Anthropic's setup, and Astra's number is OpenAI's own figure at high.

When AA ran both in the same harness:

59.6% vs 59.6%. A tie. This is the same lesson as Astra's ARC-AGI-3 score, which ARC Prize reported as 99.9% with a provider-specific harness and 62.7% with the standard one. Vendor tables are drawn under each vendor's best conditions. Read the footnotes, and prefer third-party runs that hold the harness constant.

5. Where each model actually wins

From AA at max effort:

	GPT-6 Sol	GPT-6 Astra	Claude Opus 5.5
Terminal-Bench 4.0	43.9%	59.6%	59.6%
AutomationBench-AA	61.6%	69%	69.5%
GDP.pdf (professional documents)	24.8%	31%	26.2%
Hallucination rate (lower is better)	60.1%	51%	58.6%
GDPval-AA (44 occupations, Elo)	1487	1542	1846

Opus 5.5 is far ahead on knowledge work (GDPval-AA is a ~300 Elo lead over Astra). AA's industry sub-indexes agree: finance, legal, and economics all favor Opus.
Astra leads on document reasoning and hallucinates least. In the vendors' own tables it also leads on Terminal-Bench Science (64.6% vs 58.7%, per Anthropic's table).
Astra has several claims Opus 5.5 simply hasn't been measured on: FrontierMath Tier 4 (97.6%), ScreenSpot-Pro (92.7%), MRCR v2 at 512K–1M (96.3%), ExploitBench (100%). No number means no verdict either way.
Sol is the fast, cheap one. It isn't built to win this table.

6. Latency

AA, all at medium effort:

	GPT-6 Sol	GPT-6 Astra	Claude Opus 5.5
Time to first answer token	~2.0 s	~6.2 s	~24.4 s
Output speed	~114 tok/s	~48 tok/s	~75 tok/s
Time per task	~60 s	~198 s	~206 s

For a user-facing chat UI, Sol at medium is in a different league. Crank Astra to max and you're waiting over five minutes for the first answer token.

7. Integration gotchas

Opus 5.5 can't run with thinking disabled. Effort is your only depth control. Sol offers a none reasoning setting (though AA found Sol's non-reasoning mode scored lower and cost more per task than low).
Opus 5.5 routes some requests to other models. When its safeguards trigger, most cybersecurity tasks are handled by Claude Opus 4.8. AA's numbers were measured with this default fallback on.
Astra is rated "Critical" for cyber capability under OpenAI's Preparedness Framework. It currently refuses advanced tasks like proof-of-concept exploits, and OpenAI's misalignment monitoring can stop a task outright in the API.
Mind the 272K line on OpenAI models. A prompt at 280K tokens is billed very differently from one at 270K.

8. A routing recipe you can steal

Default to Opus 5.5 medium for knowledge work and hard agent tasks. It beats Sol's best score and matches Astra high, for less.
Escalate to Opus 5.5 high only when a task fails your acceptance check, rather than starting at max.
Send high-volume, well-specified work to Sol (classification, extraction, first-line support), especially if latency matters.
Keep Astra in the pool for document-heavy reasoning, low-hallucination requirements, science and GUI-heavy work, and verify on your own tasks.

Then measure the only metric that matters, cost per shipped output, including human fix time:

from dataclasses import dataclass

@dataclass(frozen=True)
class Config:
    name: str
    cost_per_attempt: float  # USD, measured on YOUR tasks
    accept_rate: float       # share of outputs you actually ship
    fix_minutes: float       # human repair time per shipped output

def cost_per_accepted(cfg: Config, hourly_rate: float = 60.0) -> float:
    model_cost = cfg.cost_per_attempt / cfg.accept_rate
    human_cost = cfg.fix_minutes / 60 * hourly_rate
    return model_cost + human_cost

# Hypothetical numbers, just to show the shape of the math
for cfg in (
    Config("cheap config", cost_per_attempt=0.25, accept_rate=0.60, fix_minutes=12),
    Config("pricier config", cost_per_attempt=1.34, accept_rate=0.85, fix_minutes=4),
):
    print(f"{cfg.name:>15}: ${cost_per_accepted(cfg):.2f} per shipped output")

   cheap config: $12.42 per shipped output
 pricier config: $5.58 per shipped output

With any realistic hourly rate, human review time dominates the model bill. That is exactly why the "cheapest model" and the "cheapest workflow" are often different things.

Caveats

AA's tasks are not your tasks. Treat the scores as a map, not a forecast.
Costs are AA's estimates, including typical cache-hit rates.
A few per-benchmark values above are rounded integers as AA published them.
AA re-based its index since Astra launched (v4.1.1 → v4.3.2). Scores from different versions aren't comparable.

Sources

Anthropic, Introducing Claude Opus 5.5 and Pricing
OpenAI, Introducing GPT-6 Sol and Luna, GPT-6 Astra, GPT-6 Sol model page, GPT-6 Astra model page
Artificial Analysis, Opus 5.5 vs Astra, Sol vs Opus 5.5, Benchmarking GPT-6 Astra, Opus 5.5 article, Sol and Luna article

Disclosure: I researched and drafted this with help from Claude, which makes Anthropic a party to this comparison. Every figure comes from Artificial Analysis or the vendors' own pages, linked above.

Qiita (Japanese): https://qiita.com/GeneLab_999
Zenn (Japanese): https://zenn.dev/genelab_999
YouTube: https://www.youtube.com/@geneLab_999
X: https://x.com/geneLab_999

I built a Jev-style decision model for Japanese in two days. Claude Code A/B-tested my architecture and killed it.

GeneLab_999 — Tue, 22 Sep 2026 06:35:24 +0000

TL;DR

TypeSafe's Jev introduced "System One" models: no text generation, you send a state and typed questions, you get typed answers with calibrated probabilities in one forward pass. Open reproductions followed within weeks. The most complete one is Laya (ModernBERT-large, 421M).
I benchmarked laya-multilingual on 300 Japanese business emails. choice works. score (ordinal) and bool are below the majority-class baseline.
The score failure is a positional bias: the first-listed option is chosen 0 to 1 times out of 300, under five different orderings and wordings. It reproduces in English (0/290). The English laya checkpoint does not have it. Filed as NandhaKishorM/laya#131.
I built a Japanese one, sokudan-ja-310m, on ModernBERT-Ja. On the same 300 items with unseen schemas it beats laya-multilingual on all three primitives, three seeds. Model, code, benchmark and training-data recipe are public.
Day 1 produced a model that ignored the input text. Day 2 fixed the data and it still failed. The actual cause was my architecture. Claude Code, which I had handed the spec to, ran the A/B that proved it.

Model: https://huggingface.co/GeneLab/sokudan-ja-310m
Code: https://github.com/hiroki-abe-58/sokudan

What a System One model is

If you have ever asked an LLM "which department should handle this ticket, answer with one word" and then written a regex to parse the reply, you know the problem. You are using a text generator as a classifier and paying for it in latency, cost and parse failures.

A System One model skips the generation. Three question types:

type	asks	returns
choice	pick one of N options	choice, per-option probabilities, confidence
score	rate on an ordinal rubric	score, distribution, confidence
bool (Jev calls it noul)	is this statement true	P(true)

Multiple questions go in one request and are evaluated against the same state independently. Laya implements this as an encoder with one [MASK] token per option; the hidden state at each mask is scored and softmaxed within the question. Because the answer space is defined at request time, new schemas need no retraining. On an RTX 5090 it runs at 22 ms per item.

The benchmark

I generated 300 Japanese business emails with a local LLM (Qwen3 30B-A3B), label-conditioned: the prompt says "write a slightly irritated billing inquiry that hints at cancellation", so the generation conditions are the gold labels. No annotation. Three questions per document: 4-way department routing (choice), 3-level urgency (score), "hints at churn" (bool).

Baselines, all on the same 300 items with the same scoring code: laya-multilingual, laya (English checkpoint fed Japanese), majority class, random, and the generating LLM itself as a classifier (an upper bound, not a fair comparison, since it wrote the data).

I did not benchmark Jev itself. TypeSafe's Master Customer Agreement (2.3(b)) prohibits using the service or its output to develop a similar product, and this is one.

Results for laya-multilingual

	choice acc	score RPS (lower is better)	score acc	bool acc	bool AUROC
laya-multilingual	0.747	0.232	0.443	0.543	0.523
majority class	0.380	0.197	0.460	0.703	—
random	0.253	0.201	0.403	0.513	—

choice is fine: twice the majority baseline, three times random. If you need multi-class routing in Japanese, this checkpoint works today.

score is worse than always predicting the majority level. The confusion matrix explains why:

gold \ predicted	soon	work is blocked
not urgent (77)	58	19
soon (138)	78	60
work is blocked (85)	30	55

The lowest level is never predicted. My first guesses were "weak on Japanese negation" or "ordinal training is broken". Five more conditions ruled both out:

condition	options (in listed order)	first option chosen	argmax counts
A original	not urgent / soon / blocked	0 / 300	[0, 167, 133]
B reversed	blocked / soon / not urgent	0 / 300	[0, 50, 250]
C relabeled	low / mid / high	1 / 300	[1, 291, 8]
D relabeled, reversed	high / mid / low	1 / 300	[1, 0, 299]
E four levels	not at all / not urgent / soon / blocked	0 / 300	[0, 78, 37, 185]

Compare B and D. The last-listed option means "not urgent" in one and "high" in the other. Both attract most of the mass (250 and 299). The model is answering by slot, not by label.

Then I ran the same five conditions on 290 English emails, because English is a training language for this checkpoint and "it can't read the input" should not apply:

model	Japanese (n=300)	English (n=290)
laya-multilingual	0, 0, 1, 1, 0	0, 0, 0, 0, 0
laya (English checkpoint)	13, 56, 8, 1, 110	65, 74, 0, 5, 4

Still zero. In English, laya-multilingual also gets score RPS 0.340 (random is 0.197) and bool AUROC 0.355, which is below 0.5, meaning the ranking is inverted. The English checkpoint picks the first option 22 to 26 percent of the time under the same conditions. This is not a language gap; it is something specific to the multilingual checkpoint.

Practical consequence: ordinal rubrics almost always list the lowest level first. On this checkpoint, score will almost never return the lowest level regardless of input.

I verified my harness against the official laya package with laya.load() / agent.predict() straight from the README; probabilities match to float precision. Repro: docs/baseline_en.md.

Temperature scaling, for the record, fixes ECE (0.148 to 0.087) and changes no argmax at all. As expected.

So I built one

sokudan-ja-310m: sbintuitions/modernbert-ja-310m backbone (MIT), full fine-tune, one <mask> per option, softmax within the question. Two design choices worth mentioning:

score is not a multi-class softmax. It uses a cumulative-link parameterization that keeps the CDF monotone for any number of levels K, decided at request time: each level's marker contributes a non-negative increment via softplus, and P(y > k) is a sigmoid over the running sum. K=2 and K=7 share the same head.
All training data is gold-labeled synthetic data from the same label-conditioned generation. No Laya or Jev outputs anywhere.

Results on the same 300 items, three seeds, mean ± SD. The benchmark's three schemas were never in training:

	choice acc	score RPS	score acc	bool acc	bool AUROC
sokudan-ja-310m	0.847 ± 0.009	0.090 ± 0.023	0.763 ± 0.088	0.788 ± 0.010	0.789 ± 0.043
laya-multilingual	0.747	0.232	0.443	0.543	0.523
majority class	0.380	0.197	0.460	0.703	—

Seed variance on score accuracy is large (0.663 / 0.800 / 0.827). The distributed weights are seed 0, which is the worst of the three on that metric and the best on bool AUROC. Seed 0 was designated before any of the three finished training. Seeds 1 and 2 are revisions in the same repo.

Under the five position-bias conditions, sokudan picks the first option 45 to 98 times out of 300 (i.e. normally), across all seeds.

The part I actually want to write about

Day 1 ended with a model whose bool AUROC on the benchmark was 0.513. Diagnostics showed something worse than "weak": replacing the input text with an empty string improved bool accuracy (0.623 to 0.703). The model was reading the question and emitting a prior. My training data's bool questions were all mechanical derivations ("does this document belong to category X", "is urgency at least level k") and none required reading for intent. "Hints at churn" is an intent question. You cannot transfer a skill you never trained.

Day 2 morning: Claude Code and I redesigned the data. Twenty-four attributes baked into the generation prompt as conditions, split into three tiers: surface (mentions a deadline), explicit attitude (states dissatisfaction), implicit intent (implies it is about to decline). Five attributes held out entirely so we had an unseen-schema validation set that was not the benchmark. Claude Code caught two things in the verification pass that I would not have: implicit-intent attributes imply each other, so independent 50/50 sampling creates false labels that are actually true; and discarding verifier disagreements removes hard cases asymmetrically, teaching "always yes". Both fixed.

Day 2 afternoon: trained on the new data. Held-out bool AUROC 0.509. Every held-out attribute at chance, including "ends with a question mark". And choice and score were worse than Day 1 despite 2.6 times the data.

Here is the diagnostic that mattered. On attributes the model had trained on, evaluated on unseen documents, only 4 of 14 were above 0.7, and the top two were "contains numbers" and "mentions a deadline". Lexical. Every attitude and intent attribute sat at 0.5 even though the model had seen thousands of examples of each. Before asking why it did not transfer, we had to ask why it had not learned.

My architecture encoded the state and the question separately and merged them in a two-layer cross-attention head. The selling point was that the state is encoded once per request and broadcast to all questions, so latency does not grow with question count. I had rejected Laya's joint layout (question and state in one sequence) on the grounds that ModernBERT has global attention only every third layer and a 128-token local window, so a question block placed far from the state could not see it.

Claude Code proposed the A/B and ran it: same data, same mix, same epochs, same learning rate, the only change being joint encoding with no cross-attention head.

	cross-attention (mine)	joint (Laya's layout)
held-out bool AUROC, unseen schema	0.506	0.872
implicit-intent tier	0.486	0.786
explicit-attitude tier	—	0.995
trained attributes on unseen docs	4 of 14 above 0.7	14 of 14 between 0.96 and 1.00
seconds per epoch	464	330

Ablating the state (empty or shuffled) drops joint to 0.485 / 0.504. It is reading the text.

My local-attention argument was correct and irrelevant. The mean sequence length in this data is 160 tokens. The "question block at position 3000" I was worried about never occurs. Meanwhile, the only held-out attribute joint failed was "ends with a question mark" (0.688), which is a positional question and exactly where a 128-token window hurts. The concern was real; I had aimed it at the wrong place.

I retracted the design, the latency claim, and the paragraph in the architecture doc that explained why joint would not work. v0.1 ships joint. Claude Code wrote the retraction section with the A/B numbers and a note on where the original argument's premise failed.

Two things I put in the spec that earned their place: never fabricate a number, write TBD (no estimate ever leaked into a doc), and stop at the gate (three sub-majority checkpoints were stopped before publication). One thing I did not put in the spec: permission to refute the spec's author. It did that on its own.

Limits

On the benchmark, bool under-predicts true (mean P(true) 0.125 vs a gold rate of 0.297). AUROC 0.789, so the ranking works; set your threshold to your prior. Temperature does not shift this.
Calibration helps choice and bool ECE and hurts score RPS (0.090 to 0.149). Default is uncalibrated; temperatures.json is included; refit on your own validation set.
Long inputs: held-out bool AUROC drops from 0.904 on short documents to 0.730 at 400 to 800 tokens. Local attention.
Latency scales with question count under joint encoding. usage.backbone_passes in the response tells you how many.
Single benchmark, 300 items, all synthetic from one LLM. Real-data validation is next.

🛠️ I Built a One-Click ComfyUI Setup for RTX 5090 on Windows — No WSL2, No Docker

GeneLab_999 — Mon, 02 Mar 2026 15:18:28 +0000

I bought an RTX 5090. 32GB VRAM. The most powerful consumer GPU on the planet.

Then I tried to run ComfyUI on Windows. It broke immediately.

RuntimeError: sm_120 is not compatible

Three days later, I had a fully working solution. I packaged it and open-sourced it:

ComfyUI-Win-Blackwell

Here's the whole story.

Why RTX 50-series Breaks Everything

NVIDIA's Blackwell architecture (RTX 5090/5080/5070) uses a new compute capability code called sm_120. The problem? PyTorch's stable release doesn't include kernels for it.

This means:

pip install torch → doesn't work on Blackwell
You need PyTorch nightly with CUDA 13.0 (cu130)
But then xformers (the standard ComfyUI speed boost) forces PyTorch back to stable
And custom nodes silently pull stable PyTorch through their dependencies

It's a dependency trap. Every fix creates a new problem.

The 5 Rules I Discovered

After 3 days of trial and error, I distilled everything into 5 rules. Break any one of them and your environment dies.

Rule 1: Use PyTorch nightly cu130 — stable doesn't have sm_120 kernels.

Rule 2: Never install xformers — it force-downgrades PyTorch to stable. This is the trap that got me twice.

Rule 3: Strip torch from every requirements.txt — custom nodes list torch as a dependency, and pip will happily replace your nightly build with stable.

Rule 4: Verify PyTorch after every custom node install — run python -c "import torch; print(torch.__version__)" and check that it still says cu130.

Rule 5: Clear proxy environment variables — system proxies block pip and git silently on Windows.

💡 Pro Tip: Rule 2 was the hardest to figure out. xformers installs successfully, ComfyUI starts fine, and then crashes mid-inference with sm_120 is not compatible. You don't even realize PyTorch was downgraded until you check the version.

What I Built

I automated all 5 rules into a one-click setup:

git clone https://github.com/hiroki-abe-58/ComfyUI-Win-Blackwell.git
cd ComfyUI-Win-Blackwell
# Double-click setup.bat — done in ~20 minutes

What setup.bat handles:

Python 3.13 environment
PyTorch nightly cu130 (not stable, not cu128)
triton-windows + torch.compile (replaces xformers)
ComfyUI core + custom dependencies (with torch stripped out)
28 verified custom nodes
Post-install verification that cu130 is still intact

I also built companion tools:

verify_env.py — Blackwell-specific environment checker (sm_120, cu130, Triton, torch.compile)
fix_windows_compat.py — Converts Linux workflow JSON paths to Windows format, replaces SageAttention with SDPA
update.bat — Updates everything while preserving Blackwell compatibility

What I Verified

I tested 28 custom nodes one by one. Install → check PyTorch version → run test → record result. That was the most tedious part.

I also tested 5 Image-to-Video pipelines on 32GB VRAM:

HunyuanVideo 1.5 I2V (8.3B params, ~16GB) — Smooth. My top recommendation.
Kandinsky 5.0 Lite I2V (2B, ~4GB) — Very smooth. Great for quick tests.
LTX-2 I2V (19B, ~25GB) — Works in FP8. Tight but fine.
LongCat-Video TI2V (13.6B, ~14.5GB) — Works with adjustments.
Kandinsky 5.0 Pro I2V (19B, ~40GB) — Needs CPU offload. Slow.

Why Not Just Use WSL2 or Docker?

The short answer: performance.

Loading safetensors through WSL2's NTFS translation layer is noticeably slower. Docker has the same issue plus additional setup complexity. For a tool like ComfyUI where you're iterating on workflows and loading large models frequently, native Windows file I/O makes a real difference.

Also, most AI artists using ComfyUI on Windows aren't Docker experts. A .bat file they can double-click is the right UX.

Wrapping Up

If you have an RTX 5090/5080/5070 and want to run ComfyUI on Windows without WSL2 or Docker, give it a try:

github.com/hiroki-abe-58/ComfyUI-Win-Blackwell

hiroki-abe-58 / ComfyUI-Win-Blackwell

ComfyUI for GeForce RTX 50-Series (Blackwell)

The first fully documented, Windows-native ComfyUI setup for NVIDIA GeForce RTX 5090/5080/5070 (Blackwell architecture, sm_120) with CUDA 13.0.

Other languages: 日本語 | 中文 | 한국어

What Makes This Special

RTX 50-series GPUs (Blackwell, Compute Capability sm_120) are not supported by PyTorch stable releases as of early 2026. Running ComfyUI on these GPUs requires specific versions and workarounds that are not documented anywhere else in a single, reproducible package.

Technical Highlights

Feature	Details
GPU Architecture	NVIDIA Blackwell (sm_120) -- RTX 5090 / 5080 / 5070
CUDA Version	13.0 (cu130) -- the latest CUDA runtime
PyTorch	Nightly cu130 build (not stable, not cu128)
Python	3.13 (latest)
Triton	triton-windows fork (official Triton is Linux-only)
xformers	Deliberately excluded (causes PyTorch downgrade)
Custom Nodes	28 verified nodes including video & music generation
Platform	Windows Native (no WSL2, no Docker required)

Why This Is Unique

Blackwell + Windows Native +…

View on GitHub

MIT licensed. Stars and PRs welcome — especially if you verify additional custom nodes on Blackwell hardware.

Have you tried running AI tools on RTX 50-series? What was your experience? Let me know in the comments! 👇

If you found this helpful, consider following me for more AI + GPU content!

📝 Japanese version: Qiita / Zenn
🐦 Follow me on X: @geneLab_999
💻 GitHub: hiroki-abe-58

DEV Community: GeneLab_999

Proving what a URL allowlist decides, in Lean 4

What it does

The theorems

Tested against real parsers

Where the name resolves to

What it does not do

Try it

References

PathFence: A Lean 4 Path Checker—and Where Its Guarantees Stop

What the checker does

What Lean proves

Tests complement the proof

File access still needs kernel enforcement

Try it

A Small Attention Fallback Fix Cut Peak Mask-Pass VRAM by 87%

The expensive path was the fallback

The change

What I measured

Did the outputs change?

This is not a universal MHA-to-SDPA rule

Why a small default change matters

From ImportError to Video: Bringing Looking Ahead to Windows

Why I wanted to run Looking Ahead

1. Installed does not mean importable

2. Cross-attention bypassed the fallback

3. Model loading had its own Unix dependency

What the Windows run established

Preserving FA4 and comparing SDPA are different checks

The 5B follow-up found the next boundary

What I would carry into the next portability fix

Same Weights, Same Seed, Different Pixels: Porting PixRestore to ComfyUI

First, define which official run you mean

A node inherits the application's numerical settings

The last conversion is still part of inference

Make sure the parity test can fail

Exact reproduction does not guarantee a good restoration

Where the implementation stands

🛡️ Patched PHP2Shell but php -v Still Says 8.3.6? Here's How to Actually Check

TL;DR

Quick context: what is PHP2Shell?

Step 1: Record the "before" state

Step 2: Install the fix

Step 3: The gotcha 🪤

Step 4: Restart, or it didn't happen

What about mitigations if you can't patch today?

Results

Wrapping up

Sources

Separate Dialogue, Music, and Sound Effects in ComfyUI

What you can do with the three tracks

Install ComfyUI-DBS

Separate the dialogue from a video

Which model should you choose?

What I verified—and what still needs listening

Decision models are English-first. I measured them in Japanese, then built one.

1. The first thing I found: a position prior

2. Building a Japanese one

3. What transfers back to English

4. A Japanese typed-decisions benchmark

5. Things that bit me

If you're building one for your language

Links

I didn't fix the bug: contributing to a 20k-star ML repo by measuring it

What laya is, and why I was measuring it

The number that didn't fit

Making it hard to explain away

Someone else went deeper

Testing someone else's hypothesis, and my own

The maintainer's call

Handing over a tool

Before opening the PR

On using Claude Code

What I'd tell myself next time

Where it stands

131 is open, and the retrain is pending. When it lands, presentation_checks.py gives the first answer, and I'll run the labelled A–F and A/C/D before/after on top of it.

Claude Opus 5.5 vs GPT-6 Astra vs GPT-6 Sol: the effort knob matters more than the model

TL;DR

1. The price sheet (and its fine print)

2. Tokens per task is the hidden multiplier

131 is open, and the retrain is pending. When it lands, `presentation_checks.py` gives the first answer, and I'll run the labelled A–F and A/C/D before/after on top of it.