0.15.0: docs that match the code; a server hardened by a second formal pass

Docs that match the code, and a server hardened by a second formal pass. Every document was checked claim by claim against the source, and the READMEs now lead with what the memory does for you, what a day with it looks like, and an honest account of its maturity and costs. The formal pass modelled the parts added since 0.11 in Lean and fixed 26 findings (F6, F7, F13–F32, F34–F37), each reproduced against the real code and covered by a test; two more (F33, F38) are recorded as open. Background upkeep is now opt-in, the visual editor shows project changes live, and kg_put_node refuses, once, a write that would drop stored notes.

Changed

• kg_put_node refuses, once, a write that leaves out stored notes. Notes sent with a write replace the stored list, so a model that sent only its new case after a full read silently deleted the lesson's history. The write is now refused with the notes it would remove marked; the same write sent again is taken as intended, so merging or trimming notes still works.
• Background upkeep is opt-in in kg setup. It spends quota, so its question now defaults to No, and kg setup --yes applies it only when named (--only upkeep). --plan marks it. Every other item still defaults to yes.
• kg_useful's ids parameter states the real limits: five per session as guidance, ten as the hard cap, as its description already said; it read "session budget: 5 total".
• The Antigravity rule no longer says maintenance and history scouting are out of scope. Both have worked in Antigravity since 0.11.0; the stale sentence could make the model decline /kg-scout.

Added

• The visual editor shows project changes live. The page subscribes to the graph on screen, so changes an agent makes to that project now appear without Refresh, as user-graph changes already did; other projects' changes never reach it. Project changes were also addressed by the writer's session, so the editor's own project writes were broadcast to nobody; they are now addressed by the graph written. The protocol was modelled before it was built (formal/websocket/): a naive design applied an old project's change after a switch, or lost a write between load and subscribe. With an older server the page falls back to Refresh, and an older page works as before. The status reads Connected until the subscription is confirmed, then Live. Closes formal finding F6.

Fixed

• A reply's effects wait for the reply, in four more cases (formal findings F13–F16, each modelled in Lean, reproduced against the real code and covered by a test). A paged kg_read(ids=[...]) counted a node as read in full with the part showing its header, though its notes could continue in the next part; a write could then drop notes the session never received. In Antigravity, the "other sessions wrote" notice marked nodes seen before its queued reply was delivered, even when it was refused, so a write built on an older view could overwrite another session's change. A full read replayed after a compaction marked preloaded anchors seen though the new preload no longer showed them. And a compaction with a full delivery queue refused the fresh preload, so replayed replies reached the new context first.
• Background upkeep holds its limits in seven more cases (formal findings F17–F23, modelled, reproduced and tested). A timed-out Antigravity run no longer leaves agy running beside the next one. A configured codex_bin or antigravity_bin now pins its runner under "auto" even when Claude Code is installed, as promised in 0.10.0. An unwritable chore_state.json refuses instead of dispatching on every prompt. A five-hour reading carried forward from an earlier status-line frame is aged by when it was seen, not by when the file was last written. A runner command that fails to build is logged and no longer wedges dispatch until restart. The dispatch lock re-reads the config and clock, so switching chores off or changing the runner mid-decision is honoured and a long suspend cannot spend on a stale gauge or break a graph's cooldown. And an Antigravity budget notice no longer describes a window that has already reset.
• The server lifecycle holds in three more cases (formal findings F24–F26, modelled, reproduced and tested). A start that outlasted kg's wait no longer leaves its server untracked under a start-error record that made later sessions skip their preload: the server clears the record once it serves, and a later start reports a server that never answers instead of calling it running. A stale pid file is no longer trusted for an unrelated process that reused the pid, which could make kg stop kill another port's server. And kg stop/kg restart take the start lock, so a start during a stop no longer ends with nothing serving.
• Usefulness accounting holds in six more cases (formal findings F27–F32, modelled, reproduced and tested). A rename no longer lets a session endorse the same node twice. A maintenance rename keeps the node's activity time instead of resetting it to zero. A server restart no longer forgets that a session is a maintenance pass, which had let its reads promote, its credits count as use and its writes reach other sessions. A maintenance tidy no longer turns the author's own next case into a note credit. A crash no longer loses a vote's ledger entry while keeping the vote. And an instance-of edge in the maintenance graph no longer credits a user lesson.
• Archiving no longer flickers, and a small graph no longer keeps a node archived for nothing (formal findings F7 and F34, modelled in Lean, reproduced against the real store and tested). When compaction archived past the fill ceiling, refill waited for the next maintenance tick, so a node just archived and written to disk often came straight back 30 seconds later; refill now runs in the same tick. And promoting the last archived node also removes the archived section's header, which refill did not count, so a graph that fit entirely could keep one or two nodes archived indefinitely; refill now brings the whole archive back when it fits.
• Other sessions' writes are announced once, and only when they are writes (formal findings F35–F37, modelled, reproduced and tested). A rename, a node re-sent unchanged, or another session reading an archived node changes the node's version without writing anything, yet the "other sessions wrote" notice announced it as new: a maintenance pass renaming nodes made old lessons look like other sessions' fresh ones, and a change kg_sync had already listed came back. The notice now takes only content another session wrote since this session last looked. A session's own rename of a node another session had just changed hid that change from kg_sync and the notice for good; it is now listed. And in Antigravity, a reply queued for the next hook and a reply sent inline before it could both carry the same change; a reply now leaves out what a queued one already carries.
• The editor reconnects after a memory-server restart. Its WebSocket proxy kept the page's socket open when the server side closed, so the page showed Live but received nothing until reloaded. Either side closing now closes both.
• The visual editor follows the server's port and refuses cross-site requests. Its live-update proxy always connected to port 8765, so with another KG_HTTP_PORT live updates came from the wrong server (or none); it now follows MCP_SERVER_URL, as REST already did. Its CORS origins follow EDITOR_PORT instead of a fixed 8766. And like the memory server since 0.9.44, it refuses requests a browser marks as cross-site, so a web page can no longer make it promote a node through the proxy; a link to the editor from another site still opens its page.
• A start through the systemd unit clears an old start error. The hooks read last_start_error as "down and failing" and stop trying to start the server; only a start without the unit cleared it. A start through the unit now clears it on success and records the failure, pointing at the journal, when it fails. The unit now keeps XDG_STATE_HOME, so its server looks for the record where kg writes it.
• kg logs reads the journal under the systemd service. The service's server logs to stderr, which systemd keeps in the journal, but kg logs tailed the file only a server started by kg start writes, so it showed a stale log or none. With the unit enabled it now runs journalctl --user -u kg-memory.service (the file, when journalctl is missing).
• Re-running the install script upgrades kg, and it no longer fails in an agent's shell. uv tool install succeeds on an installed tool without upgrading it, so the script's upgrade fallback never ran; it now uses uv tool install --upgrade. And /dev/tty can exist without a controlling terminal, so the script tried to run kg setup there and exited with an error after installing; it now checks that the terminal opens, and otherwise says to run kg setup in a terminal.

Security

• Codex budget notices read only a rollout under home. The quota gauge read the tail of whatever transcript path a hook request named. It now goes through the same containment as every other transcript read: a .jsonl file under the user's home, or under CODEX_HOME when that lives elsewhere.

Documentation

• The READMEs now lead with what the memory does for you, what a day with it looks like, and an honest account of its maturity and costs. Docs are aligned with the current source: what kg setup offers (auto-update, auto-memory off, the kg gauge status line, background upkeep) and how kg update and kg uninstall replace the manual plugin steps; .mcp.json launching kg mcp; logs under systemd; where environment variables take effect; Windows unsupported; macOS CI report-only; transport through kg mcp and all four clients in ARCHITECTURE.md; development paths through cli/kg-dev. The plugin README's links are absolute, so they work on PyPI.
• The kg-core and kg-maintain skills drop two stale operational lines: a connection failure is no longer "the server warming up" (kg mcp starts it), and a long kg_read arrives in parts (more=true). Skill examples pass the required session_id.