#tool

roundstorm’s desktop app now generates 32 random bytes on every launch, hands them to the daemon as ROUNDSTORM_TOKEN and injects them into its own page, and the daemon refuses /api and /ws without it — unset, the headless CLI and every script behave exactly as before. It is narrower than “auth”, and SECURITY.md now says so: it stops another process on the loopback socket and another user on a shared machine, and makes ROUNDSTORM_HOST=0.0.0.0 defensible, but not malware running as the user (17618e7).

deck-lovers’ /ws disconnect cleanup ran unshielded, so a cancelled task could skip telling the audience the projector had left and leave stale clients behind — Starlette’s TestClient cancels the app task right after sending the disconnect, which made the websocket tests hang about four runs in ten. The cleanup is now wrapped in a shielded anyio cancel scope, two test races are gone, and a regression test cancels the handler the way the client does (3c4e938).

cdclkit’s target-phase search copied the whole trail into the target at every new deepest trail. The comment said improvements become rare quickly, which is true once conflicts start and false before: a search that makes many decisions without one improves on every decision, so n decisions copied 1, 2, …, n entries — 65,536 declared variables and one unit clause took 144 s in Python, 131,072 took 4.2 s natively, and each 4× in variables cost about 13–19× (e43a4ac). A counter now records how much of the trail the target already holds, only the new suffix is copied, and the target still ends up byte-for-byte what the full copy produced.

A Dependabot pull request that failed one Ubuntu cell with “database is locked” was not the bump’s fault. Importing nearly anything under server/src imports db.ts, which opens a SQLite file at import, and ten test files never set ROUNDSTORM_DATA first — so they opened the default data directory, the real database on a developer’s machine, and on CI one file shared by every parallel test process racing to create and migrate it (44a5bd9). A second bug surfaced in the same empty-HOME experiment: gate.test.ts called /api/bootstrap, which probes every brain, so npm test executed the real agy and cursor-agent CLIs on any machine that had them. scripts/test-setup.mjs is now preloaded into every test process and hands each its own empty data directory rather than relying on the next author to remember, gate.test.ts hits /api/memory instead, and a re-run under an empty HOME passes 196 of 196 while creating nothing there.

Sprint 6 of consilean measured token-free transport across the seed bridge and merged it: the H4 amendment freezes the match rule before the run, and every table stays on the pinned corpora (38eb8c7, PR #7). A second sprint recorded a preregistered H3 precision at k on the Mathlib v4.28.0 snapshot — the candidate set fixed before the run, with the neighbor-recall table kept in place (2a751b5, PR #8).

roundstorm is now public at v0.1.0: a local-first app where persistent, heterogeneous AI researchers deliberate for a set number of rounds on a hard question — you write the question once, they do the arguing. The download is a macOS Apple Silicon image, with the daemon runnable on Linux and Windows; the app bundles no models and no keys, needs Node 22.16 or newer and at least one installed, signed-in CLI brain (claude, codex, agy or cursor-agent), and the release notes state the limits rather than let them be discovered — not notarised, no authentication (the daemon listens on loopback and refuses website origins, which is not auth), advisory capability tiers, and Windows never actually run. The release-day work was a pre-public tune: CI, a real CSP, and a Node floor corrected to a 22.16 that CI measured rather than guessed (4c98425, 73568f8), the daemon moved to Express 5, CSS imports declared so the project type-checks under TypeScript 7, dependency updates taken where safe with Tauri held at 2.11 on purpose, and one open advisory recorded with why it does not reach the shipped app.

dratify 0.1.6 fixed the README’s PySAT example — it loaded formulas with PySAT’s own parser, which stops at the % line every SATLIB file ends with — and closed a release path that let workflow_dispatch publish from a branch, with the pypi and crates environments now restricted to v* tags (108dd50, 5d0bb47). 0.1.7 is the security fix: three checker bugs found while tracing why PySAT’s CaDiCaL proofs do not verify, one of them a soundness hole where the pure-Python checker accepted refutations of satisfiable formulas when a list of steps held a negative literal — reachable through check_proof, though not from cdclkit’s own solver, and text proofs were never affected — alongside an unbounded literal that could size arrays for 10¹¹ variables and two false rejections, both checkers refusing valid proofs in which a lemma arrived unit at the root (61165f9). The PySAT failure itself is not the checker’s: the binding reads every CaDiCaL proof before flushing it, and with the documented workaround all four CaDiCaL versions verify 50 of 50, where glucose and Lingeling already did (2823854).

cdclkit 0.1.4 moves both halves onto dratify>=0.1.7, whose three fixed checker bugs include two that reach this package: --self-check could reject a valid proof, and the pure-Python checker could accept a refutation through check_proof (d33f84a). Publishing is now tag-only — the environment restricted to v* tags, the workflow_dispatch trigger gone, and the version check failing outright on any other ref — and make smoke, broken since the dratify split, now ties its module list to the source tree, with a packaging CI job that builds the wheel, installs it cleanly and runs it (b7b5426). Python 3.15 rc3 joins the test matrix (including a native-engine leg) and the README example is now executed by a test; the runbook’s recorded Sigstore gap was already covered, since every file on PyPI has carried a PEP 740 attestation since the first Trusted Publishing release.

forgepulse publishes two rankings of the same fleet — human attention, built from unique views, external referrers and new stars and forks, and raw clone volume — and they rarely agree, so a repository that reaches the top ten of both now carries an award badge beside its rank, in either view (55028f2). The condition lives in web/src/lib/rank.ts as inBothTopN, which is true only when the attention rank exists and both ranks are 10 or better; the badge is styled in styles.css and the rule is covered by rank.test.ts.

A scheduled notify pass in topshift-trend can now fail halfway without repeating itself: per-chat deliveries are recorded as they succeed, so the next run skips the links a chat already received and retries only the ones that never went out, and the global cooldown baseline advances only after a clean pass (0ce1688, PR #9). Before this, one transient Telegram error in the middle of a batch could resend everything that had already arrived. A ruff UP035 fix — Mapping imported from collections.abc — rode along.

pacenotch notices that Claude Code has refreshed its OAuth token by fingerprinting the credentials it reads, and that fingerprint used to be a SHA-256 of the access token — which CodeQL flagged as go/weak-sensitive-data-hashing (a63ee1f). The hash never left memory, but hashing the secret was never needed to detect a refresh: the fingerprint is now claudeAiOauth.expiresAt, a value every refresh moves and which is not secret at all, while a PACENOTCH_TOKEN cannot change while the program runs and gets a fixed fingerprint. It is the second CodeQL-driven correction in pacenotch’s credential layer after the recovery path stopped re-reading the token.

forgepulse can now answer “who starred what, and when” across the whole fleet: a new /stars page lists every star across every tracked repository in one chronological feed — avatar, who, which repository, when — which GitHub only offers per repository and never across an account (af4a8ea). The backend adds a star_events table populated from each repository’s /stargazers endpoint requested with the star+json media type, which carries the true starred_at per user and so needs no backfill wait, unlike the human-attention baselines; it syncs alongside the existing star count.

deck-lovers’ /login handler set the proj_auth cookie to the projector password itself, so the plaintext password lived in every presenter’s browser — which CodeQL reports as py/clear-text-storage-sensitive-data. The server now issues a random per-process session token and compares password and cookie in constant time, which also means a server restart invalidates existing projector cookies; two converter test assertions that matched the bare fonts.googleapis.com hostname (py/incomplete-url-substring-sanitization) now check the exact stylesheet URL built by google_fonts_css_url() (fa4dfce).

consilean is a new public Python repository that scores pairs of formal statements in Lean corpora on two axes — how similar they are, and how far apart they sit in the dependency graph. Similar statements that sit near each other are duplicate candidates; similar statements that sit far apart are candidate hidden connections, and Lean’s kernel stays the authority on whether a connection holds: a similarity score is a pattern, not a claim.

Sprint 2 of consilean — the scorer of Lean statement pairs by similarity and dependency-graph distance, with the kernel left as the authority on whether a candidate connection holds — recorded a second H2 ranking and a read-only replay of the H3 axis against Mathlib v4.28.0, with the run reports generated into docs/ (1592971). One negative result is recorded rather than buried: the frozen Mathlib deprecation pairs cannot serve as later H3 links, because every since date is already earlier than the Mathlib revision that was scored (39a5a75). The wider statement reader therefore stays on the frozen deprecation set, and the duplicate list stays empty — none of the recovered pairs closed on the later revision.

portcullis replaced paramiko’s AutoAddPolicy — which accepts whatever key a host presents — with an explicit trust-on-first-use policy (25da71b). Phase 1 is the first contact with a VM created seconds earlier by the same process, so there is no prior key to compare against and Hetzner does not publish the fingerprint through its API: the new policy accepts that first key once, logs its type and fingerprint, and Phase 2 still connects with that exact key pinned, so a later substitution is detected. The change addresses CodeQL’s py/paramiko-missing-host-key-validation alert, and the test that asserted the blanket policy now asserts the new one. The secret-handling pass of 21 September had already pinned the key Phase 2 connects with; the first contact was still an unconditional accept.

The window columns in forgepulse were mostly empty at their recent end: GitHub’s traffic API lags a day or more, so counting back from the wall clock left the newest days without rows and the 1d column read zero for nearly every repository (7f5acb4). The windows now count back from the newest day that at least half of all repositories have a row for, and each window is capped at that day, so a stray early same-day row cannot leak in as a partial day or move the anchor — a plain MAX(day) would let one early reporter blank out everyone else. It also makes 1d genuinely one day: the old >= now − 1 day spanned up to two. It is the same lag the per-repository clone baselines were added for, now fixed at the window itself rather than at the comparison.

Podman only reports a host-port clash after the images are built, and only as an opaque “proxy already running” error that never names the port. The deploy script in deck-lovers now runs a pre-flight check in local serve mode before the build, naming the container or host process that is actually holding the port — 80 and 443 included when Caddy is started — while skipping this compose project’s own containers, so re-running over a live deck-lovers server still attaches instead of failing (5c07394).

portcullis hardened its own handling of the secrets it moves around during provisioning (f41693f): it no longer logs the first and last four characters of HCLOUD_TOKEN, keys/id_rsa is created 0600 from the start rather than being written and then narrowed, and the smtp.env values are shell-quoted before Phase 2 sources them as root — passwords containing $, spaces, quotes or backticks had been mangled or executed, and the file is now chmod 0600 on the VM before credentials are written into it. Phase 1’s SSH host key is pinned and Phase 2 rejects a different one immediately, so a swapped host cannot receive the second phase’s credentials, and preflight validation now runs before any Hetzner resource exists.

The echarts 5 → 6 bump in forgepulse changed the default legend position from top to bottom, so on both charts the legend collided with the x-axis date labels while the 48px the grid reserves at the top sat empty — legend.top is now set explicitly, so the layout stops depending on a library default (94fb8c1). The same release draws a filled marker on every data point, which on a hundred-day series is clutter; the dots are hidden on all eight series through one shared base while the axis tooltip still marks the hovered point (1f70b65). Both rode in with the vitest 4.1.11 / echarts 6.1.0 security bump.

fleetlens is now public: for a handful of Debian/Ubuntu VMs it logs in over SSH with Ansible, collects a fixed set of read-only facts and turns them into a JSON report, a Markdown report, a terminal summary and an optional email — nothing installed on the targets and nothing on them changed. It sits between “I SSH in and look around every few weeks” and a full monitoring stack: disk usage, pending updates, reboot-required, failed units and journal errors, with each host marked OK, WARNING or CRITICAL and the fleet taking the worst of them.

Seven repositories that had no continuous integration now run their own tests on every push: topshift-trend (running ruff and pytest), caciarabot and python-hosts-checker (pytest), euclean (pytest together with its Lean build), and quadratula, unstated-conclusions and prove2me-logs with smoke tests — in prove2me-logs’ case covering the p2m helper, the piece the mission journal is actually read through.

slop-audit spent the rest of the week being made presentable rather than more capable. A brush-up design split the work into Phase 1 (docs and packaging) and Phase 2 (hygiene), and Phase 1 followed: an MIT license, a changelog and pyproject.toml metadata (e7bc0a3) with the README polished and GitHub publication marked done (9b6a418), merged as PR #1.

portcullis is a new public Python repository: one command creates a hardened Ubuntu 26.04 VM on Hetzner Cloud, and it drops the gate first — an unprivileged user with key-only SSH on a random high port, root locked, UFW default-deny and sysctl hardening, all inside about 30 seconds and using only what the stock image already ships — then switches the Hetzner firewall to the new port and deletes the temporary API key before the full CIS-style pass (package upgrades, AppArmor, auditd, AIDE, PAM policy, fail2ban, rkhunter, msmtp alerts, Docker and Podman) runs behind both firewalls. verify.sh then runs 58 checks on the finished host. Everything runs inside a Podman container so nothing is installed locally, and teardown deletes a half-provisioned server together with the keys and firewalls it created. The README was rebranded as the repository went public, with a GitHub Actions test workflow on actions/checkout@v5 and a logo.

The rank-trend arrows in forgepulse’s Repository signal table cost every row its bottom border alignment: display: flex on .rank-share, added to stack the arrow, pulled that <td> out of table layout, so it stopped growing to the row’s real height and stayed clipped to its own content while the Name column stretched normally for longer descriptions. Dropping the flex display and keeping the existing block-span stacking restores the alignment — two lines of CSS, which is what a change made to fit a two-character indicator should have cost in the first place.

The clone-trend arrows added to forgepulse two days ago were reading “stable” almost everywhere, and the cause was GitHub’s traffic API rather than the repositories: it reports a day’s row inconsistently per repository, so at any moment only a handful have a same-day daily_traffic entry while most lag behind, and a single fleet-wide “yesterday” cutoff therefore compares most repositories against data already included in their current total (762ea7b). The fix is to compare each repository’s clone total against one day before that repository’s own most recent row, computed in one query through a per-repository MAX(day), so the comparison never depends on a shared calendar date — verified live, the trends now show real up and down movement instead of universal stability.

pacenotch’s GUI grew the controls a .app cannot be handed on the command line: a Settings window (footer button, tray menu, pacenotch → Settings… on macOS) for the on-pace band, the refresh interval, notifications, compact mode, appearance and Dock behaviour, applied and saved as they change (13dc75f). Because a MacBook’s camera notch can hide the menu bar icon and with it the only Quit, the app can now switch to the Regular activation policy and live in the Dock and Cmd-Tab with a Quit in the window and a Settings window that is not hidden by the notch (b6f4031).

forgepulse’s Repository signal table now carries a Billboard-chart-style up / down / stable indicator on every row, in both ranking modes, showing whether a repository moved since yesterday (9306fec). It tracks rank rather than the raw figure on purpose: clone volume ranks by total_clones, a cumulative counter that only ever grows, so diffing the value would read “up” almost every day regardless of real trend, while rank stays relative and keeps meaning.

slop-audit is now public: a Python harness that scores a piece of prose for AI-slop and formulaic style, general writing issues and descriptive stats, and — kept strictly separate from all of it — local AI-authorship detector signals. Nothing leaves the machine: there are no hosted detector APIs and no remote LLM touching the target text, with the network used only for installs and optional model-weight downloads. A run produces a Slop Index (0–100 plus band) from the slop tools and linters (05e1527), deterministic edit suggestions quoted from the tools that would lower it — no LLM rewrite of the prose (7bcdcc3) — and a per-tool matrix reporting OK / NOT_RUN / ERROR with the exact reason, so a tool that failed never invents a score.

forgepulse grew the two controls its dashboard was missing: Refresh re-fetches the stored dashboard and detail data without touching GitHub at all, while Sync now performs a real pull through the existing POST /api/v1/sync endpoint outside the hourly schedule and now surfaces the server’s error inline — an expired token says so immediately instead of failing silently until the next scheduled attempt (87cfe54). On-demand sync then exposed a contention bug worth fixing properly: the scheduled tick and the new endpoint shared one GitHub collector with no coordination, so a click landing during the hourly run let multiple full 84-repo syncs proceed at once, each with its own bounded per-repo fetch — enough load to trip secondary rate limiting and queue on SQLite’s single writer, turning overlap into a crawl rather than an error. A single-flight guard now rejects the second sync instead of letting the two contend (47b2e73).

pacenotch is a new public Go repository: a CLI, tray icon and window for macOS, Windows and Linux that reports Claude’s usage windows (5-hour session, 7-day all models, and the 7-day Sonnet/Opus windows when the plan reports them) with a thin vertical notch drawn at the elapsed fraction of each window — the fill is past the notch when you are ahead of an even pace, short of it when there is room left, and the tray icon turns red on that side of the line (d7d6da6, 371aefc). The first day of commits also landed the usage/pace packages and terminal renderer with a compact mode below 60 columns, parity and coverage tooling, and a CI matrix with packaging and the README (b8f822a, b6c6151). The macOS build learned to raise its window in front of other apps and to reopen it when the running app is launched again (9f9aa5e, 6ca1263). MIT-licensed and unofficial — not affiliated with Anthropic.

topshift-trend, the Telegram bot that watches GitHub’s monthly trending list, learned to suppress repositories it recently notified: a repo that drops out of the top-N and comes back used to announce itself to every subscriber again. The bot now keeps a notification_history.json alongside its state and subscribers, and the scheduled check filters out keys seen inside a configurable window — NOTIFICATION_COOLDOWN_DAYS, default 30 days, 0 disables the suppression. The commit touches the config, store and main loop plus three test files, and the check’s log line now reports how many entries were suppressed next to how many notifications actually went out.

forgepulse shows the age of its own data: the homepage now reads the most recent successful sync run — already recorded in the sync_runs table but never surfaced — and renders it next to the git-ref pill as Updated <UTC> · <local> (Xh Ym ago), ticking every minute (d4c5e85). Traffic history is only as useful as the moment it was collected, and until now the dashboard gave no way to tell a stale snapshot from a fresh one. The change touches two new frontend modules plus tests for the relative-time formatter and the API field behind it.

portcullis hardens a fresh Ubuntu host, and hardening has to leave the machine pleasant to actually use: Ubuntu’s Vim defaults enable xterm mouse reporting, so on a remote terminal Vim captures the selection and ordinary copy/paste stops working. A new Phase 2 section, 1.6a — Terminal editor defaults, now ships /etc/vim/vimrc.local with set mouse= (and a note in the README’s Phase 2 list), leaving selection to the terminal emulator while anyone who wants Vim’s mouse support can opt back in.

dratify tagged v0.1.4 and v0.1.5 after an audit of its published numbers: the README’s speed table came from CNF files that are not in the repository, and its “~18x” was the top of a range quoted as the typical value. A committed benchmark script (bench/repro.py) now produces figures anyone can reproduce — a second run held the geometric mean at ~15x while individual ratios moved between 11x and 22x, so the release quotes the mean and states the spread as a spread. The same pass (c34c31b) added a fuzz workflow and stopped error messages from reporting version skew in the vocabulary of an unrelated project’s module.

cdclkit tagged v0.1.3: the release leads with the bug that mattered — --adaptive --self-check printed s UNSATISFIABLE while verifying nothing. Both engines now require dratify 0.1.4, with a test that fails if they ever ask for different versions again. The same pass rewrote the docs to describe the program (a fresh make test failed with 24 import errors while the Makefile still claimed no dependencies), and BENCHMARKS.md now says what the published 20.1x figure is a sample of: one run per instance, with individual ratios seen moving by a third between runs while the geometric mean held.

dratify is tagged v0.1.3: the docs said the Python checker and the Rust checker were compared against DRATChecker on acceptances and rejections, but the only two tests that did so had silently skipped on every run — an import-time guard — so that claim had never once been exercised. The new differential suite (2889df3) sweeps 150 random instances plus hand-written accept/reject cases, and CI installs the native checker and fails if the tests skip. The same release hardens the untrusted-input paths: header counts like p cnf 99999999999 0 that would have asked for hundreds of gigabytes are rejected outright, register_native validates the checker it is handed instead of unpacking a fixed tuple, and proof parsing reports the offending line and token. Tests go from 87 to 96 and coverage 84% to 87%, with each new guard confirmed to fail when its fix is reverted.

parsimagma is tagged v1.0-stage2: one standard-library-only Python file — no database, no lookup table, no LLM call — reaches 200/200 on the organizer’s 200-problem sample set, confirmed by two independent runs agreeing problem for problem and explicitly not the private graded set. Three search mechanisms split the work: finite model search refutes false implications cell by cell, critical-pair completion proves most of the true ones, and ordered superposition under a Knuth–Bendix ordering takes the rest. Every derived equation carries its replayable derivation, paths are double-checked before any Lean is written, and certificates are emitted from the inference DAG rather than flattened — 13,728 bytes against 3,634,949 on the hardest problem.

forgepulse merged its first pull request, PR #1: human attention is now the default explainable ranking alongside clone volume. The dashboard persists fork history, collects release/tag and Actions-checkout signals, and shows each traffic diagnosis with its evidence inline. Clone-volume mode also gained sortable Stars/Views/Clones column headers (c69739b).

kiwifarmit/cra-lab is now public — a small lab in the Kiwifarm org that builds the pipeline half of a Cyber Resilience Act story instead of describing it. Pull requests go through Semgrep SAST plus SCA and IaC scanning (Semgrep rather than CodeQL, which needs GitHub Advanced Security on private repos, and it runs entirely on the runner so the code never leaves it); a v* tag generates a CycloneDX SBOM with Syft, hashes it, hands the digest to the SLSA generic generator for provenance, and runs Trivy over the release SBOM at CRITICAL/HIGH before attaching it to the release (pr-security.yml, release-security.yml). A weekly Trivy and Semgrep sweep covers vulnerability, misconfiguration and licence scanning on a timer, and Dependabot keeps the actions the workflows themselves depend on pinned, with each workflow’s comments citing the CRA Annex I Part II clause it answers.

dratify’s release pipeline could report a successful release that published nothing: ci.yml triggers on branches and pull requests and never on tags, so no test ever ran against the ref being published, and combined with skip-existing a tag that forgot to bump the version built the old one, had PyPI skip it as already present, and exited green. The suite now runs on the tag, and the build fails when the tag does not name the version it produced — skip-existing should absorb a re-run of the same release, not disguise a forgotten bump.

forgepulse hit its first tagged release, v0.1.0: the self-hosted GitHub traffic dashboard with retained clone and view history, repository analytics, charts, referrer and path snapshots, and JSONL export. The release note frames it explicitly as the baseline before the next feature — human attention ranking, which is already landing on the develop branch.

forgepulse now highlights repositories whose clone counts sit above the fleet’s median, and the comparison was fixed to use each repo’s own daily median against the fleet’s rather than its raw total, so a busy repo can no longer skew its own marker.

dratify is a new public DRAT/DRUP proof checker that runs inside your Python process: zero dependencies, no subprocess, no compiler. It replays a solver’s derived-clause log to confirm the empty clause really follows, sharing no code with the solver that wrote the proof, and the same checker is published as a Rust crate. A register_native() seam lets the Rust engine (~18x faster) be supplied without shipping a toolchain, publishing is tokenless via Trusted Publishing, and the checker’s own tests went from 12 to 71 with a coverage gate.

cdclkit is a new public CDCL SAT solver, preprocessor and encoding library, written from scratch in readable Python with an optional Rust engine (roughly 18x faster) shipped as cdclkit-native. Every answer comes with a certificate: a satisfying model is re-evaluated clause by clause, and an UNSAT answer emits a DRAT proof that an independent checker replays. It publishes on PyPI with no third-party code, and the tutorial walks one problem end to end, from DIMACS through the files between stages.

parsimagma-greedy-cover is now public on the SAIR Contributor Network, entered into the Mathematics Distillation Challenge Stage 2. It is a deterministic refuter with no LLM calls: given two equational laws it finds a finite magma satisfying the first and violating the second, and emits a Lean 4 certificate the organisers’ judge accepts under plain decide. The point of publishing is the ordering rather than the score — four instances of Z/2 refute 11,871,871 of the ETP’s 13,855,357 false implications, twenty-five refute 97.2%, and x ◇ y = 7x + 7y over Z/13 alone refutes 268 pairs that Vampire’s fmb, Mace4 and z3 on a ground encoding all fail to find. The honest number is on the item: 55 of 200 on the graded distribution, zero on the true half by design, and zero on the extra_hard category, which is selected against exactly this method.

parsimagma is a new public signature and coverage engine over the 4,694 equational laws of the Equational Theories Project, asking which ETP constructions cover which separations. Its central finding is that the residual is not uniformly hard: at least 411 of the 1,062 Vampire-unresolved implications have finite countermodels on 9 to 32 elements, found in seconds by a structured algebraic sweep where three SAT/SMT-style solvers all fail from carrier 11 upward. The repo also argues the published count of unresolved implications sits below a provable floor and independently reproduces corrected figures for the paper’s section 5.1.

The Equational Theories Project’s completed implication graph turns out to be fetchable: finite_graph.json and graph.json are build artifacts the site serves and the repository does not track, and decoding them reproduces the project dashboard exactly, recovering its two remaining open cells, (677, 255) and its dual, without being told. That splits the 1,062 Vampire-unresolved implications precisely — 610 require an infinite model, 450 have a finite counterexample, 2 are still open — which settles the question parsimagma had filed as unanswerable in issue #1474, and corrects its own headline: 610 of those 1,062 admit no finite counterexample at all, so the corpus reaches 411 of 450, not 411 of 1,062. Same measurement, 39% or 91% depending on which denominator you bother to compute. The earlier claim that the circulating figure of 310 sits below a provable floor is withdrawn: counted up to duality the same set is 316, so 310 looks like a dual-class count against an earlier snapshot rather than an error. The graph is also Lean-verified, so it can contradict the engine, and does not: 790 of 790 finite witnesses agree, and 19,392 order-5 laws extracted from a fork’s branch agree too.

erdos-straus-offset-lean now carries a Palomar submission surface on its palomar branch: a Challenge.lean statement surface, a Solution.lean with the proved counterparts, and a comparator that audits the pair, pinned to Lean/Mathlib v4.32.0. The Comparator result recorded in formalization.yaml passed on both kernels — Lean’s default kernel and the independent NanoDa kernel accept the four compared theorems, with the axiom closure limited to propext, Classical.choice, and Quot.sound. The metadata file also declares the automation method as an agent (Claude Opus 5 High via Claude Code).

forgepulse fixed two web-UI bugs: opening a repository detail page directly, or in a new tab, no longer 404s, and modifier-clicking a link now opens it in a new tab instead of swallowing the click. CI was retriggered after a GitHub Actions outage stalled the pipeline.

The pull request adding selectable daily clone statistics to hrodrig/gghstats was merged upstream: the “Unique” line on the clones-over-time chart and the compact daily clone panel are now part of the project.

forgepulse’s repository detail page now links its title, top referrers, and popular paths straight to GitHub (paths always, referrers only when they look like real hostnames), and the JSONL export filename embeds a UTC timestamp so re-downloads stop silently overwriting the previous file. A cross-check against the issues opened on hrodrig/gghstats found that three of them applied to forgepulse too — the export filename, the stats-panel jargon, and the rank column header — and were fixed here; the locale-formatting issue does not apply in the same shape yet.

forgepulse got its launch-week pass: the repository table is paginated, a favicon landed, and the static “LOCAL” badge now shows the running git ref. On the ops side, a scheduled sync that was silently failing (the /data volume was never chowned to the app user) and a repository detail page that replayed every historical referrer day are fixed, and the production container now restarts itself after a crash or reboot.

forgepulse is now public: a self-hosted GitHub traffic-history analytics app built with Rust, a Svelte frontend, SQLite for storage, and Podman for deployment. It keeps a running history of GitHub traffic metrics so trends accumulate instead of vanishing after GitHub’s rolling window.

Contributed to hrodrig/gghstats with a pull request that adds selectable daily clone statistics to the repository index: a second “Unique” line on the clones-over-time chart with its legend enabled, plus a compact daily clone panel. The change makes unique cloners visible alongside total clone events.

dash parses DMARC aggregate reports in a serverless setup for Gmail: it extracts and parses incoming reports, enriches the failing sources, and emails a summary of which senders are failing DMARC and why. The repo is public and actively developed.

spriter is a new browser-only tool that turns a raster image into a pixel-art sprite. There’s no upload, no build step, and no dependencies — the whole conversion happens locally in the browser.