~/software
[ 30 repos ] platform · main dependency · install under each // hover to preview
Machine-checked software04
- PithA formally verified application core that a coding agent builds an application around, with a judge that says exactly which properties of the result are proved, model-checked, tested, or awaiting human review. The seed holds a Dafny-proven authorization-and-reservation kernel, the obligations every surrounding layer must satisfy (TLA+ invariants, black-box harnesses, a UI contract), and an evaluator that runs the candidate as a separate process and never trusts its output. Research prototype: four external reviews and one unassisted agent build so far, and a green result does not mean the application is correct.
- HN, formallyhn-formalThe Hacker News front page and its 30 threads, rendered by a Lean 4 program proven to render every API input correctly, and redesigned every night by an LLM loop that releases without human review whenever a candidate passes. Structure, data fidelity and the no-injection property are proven; contrast, reflow and accessibility are checked per release in a browser and never called proven.
- FaithfulfaithfulMake one TypeScript function faster and see exactly how much of “it still does the same thing” was checked. Each rewrite must compile, stay pure, match the original on generated inputs, survive a bounded Z3 search and benchmark faster; one that is significantly faster is then proved in Lean 4 against a spec agreed in plain words. Every result carries one of five labels. Early: the translator accepts 39 of 74 corpus functions and 0 of 20 sampled from real libraries; in the launch campaign, 3 of 130 candidate rewrites were accepted with a proof and 72 were faster but not proved.
- UndefinedundefinedA live program that grows the functions you call but haven’t written. Bring a spreadsheet export and ask a question: a model drafts the calculation and the checks it must pass, asks what the question leaves open, and you approve the checks before anything counts. A strict TypeScript compiler, unit and property tests, and purity and time-limit gates then decide what is accepted, and only an answer that passes them all is shown; a mutation check reports which bugs those checks would miss. The same engine runs as a CLI and a GitHub Action that certify TypeScript from any source.
Research code09
- Claim-correctness probes / ProbeMonactivation-probes-claim-correctnessResearch code and two domain-specific probes (legal QA, biographies) for comparing Llama 3.1 8B’s hidden-state correctness signal with its stated confidence.
- Qwen Scope Labqwen-scope-labA browser-based workbench for sparse-autoencoder interpretability on Qwen3.5-2B: inspect features token by token, steer generation, and test detectors against controls. The model and its SAE run on the Mac through MLX.
- Block-sparse steeringbsf-steeringTrains a block-sparse dictionary on Qwen3.5-2B-Base’s layer-14 activations and tests steering with it against SAE features, difference-of-means and random directions, under a preregistered plan. Of five concepts, only medical vocabulary beat the difference-of-means and random baselines on held-out words, and 40% of those continuations fell into repetition loops. The SAE baseline failed its liveness check on every concept, so it gave no valid comparison.
- Panel-style reasoningmulti-modelTraining and evaluation code for an exploratory comparison of a panel-format Qwen3-30B-A3B adapter with Qwen’s thinking mode, plus its RL follow-up. Written up in two posts.
- Society of Thoughtsociety-of-thought-benchA preview adapter and synthetic evaluation suite (Countdown, evidence verdicts) for inspecting visible multi-persona reasoning.
- Hypothesis Forgehypothesis_forgeAn RL environment that scores proposed hypotheses on grounding, novelty, and the experiments that could falsify them.
- Adaptive retrieval experimentsadaptive_rag_rlmTest adaptive recursive search against fixed retrieval pipelines on procedurally generated document collections.
- autoresearch-evoAdds run memory, novelty-oriented search, and agent review to autoresearch’s training-code experiments.
- ProofgradeA first-pass reviewer for olympiad-style proofs, using an official solution and rubric. Includes benchmark results, a command-line tool, and a local API.
ML on Apple Silicon04
- nanochat-mlxTrain a small chatbot from scratch on Apple Silicon, from tokenizer training to a chat interface.
- Gemma 4 on a 24GB MacBookgemma4-m4-proMeasured runtime configurations, memory use, and fallback options for Gemma 4 26B A4B on an M4 Pro MacBook.
- Gemma 4 Sudoku on MLXtrain-gemma4-sudoku-on-your-macbookRun a Sudoku reinforcement-learning notebook for Gemma 4 E2B locally on Apple Silicon.
- TTT-Discover on MLXttt-discover-autoresearch-mlxSearch for improvements to training code with an RL outer loop, evaluating candidates locally on Apple Silicon.
Agent tooling02
- Dynamic Workflows on Codexclaude-dynamic-workflows-codexA Claude Code skill: describe a task, and Claude writes a multi-agent workflow script, runs it on Codex agents instead of Claude subagents, and shows the run as a live map. Agents edit files without asking unless the run is read-only.
- Flightdeckclaude-flightdeckA Claude Code mod that puts a live agent dashboard in your terminal: context and cost, an advisor timeline, every permission check, and your subagents as cards or swimlanes. It only watches: every hook passes its event on unchanged, and it never denies, rewrites or delays a tool call.
macOS utilities11
- SunShiftAdjust Night Shift warmth directly from the menu bar.
- TabPilotFind duplicate and stale Safari tabs, search open pages, and group tabs by domain.
- SafariMarkdownTurn the current Safari page into Markdown using Codex.
- GhostLabelGive Ghostty tabs descriptive titles using Codex.
- PasteForgeReformat, encode, hash, and inspect clipboard text from the menu bar.
- TextDropPaste text into a minimal editor and save it as a file. You type the extension in the save dialog.
- ClipDropOpens with the clipboard’s text already loaded. Edit it and save it as Markdown, code, JSON, or one of the other supported text types.
- DiskPulseCheck used and available space on each connected drive.
- PortSentrySee which processes own listening TCP ports and stop them from the menu bar.
- ProcessBeaconGet notified when a long-running process finishes.
- BrewPilotStart, stop, and restart Homebrew services from the menu bar.