MuseWeaver

MuseWeaver (https://aariv.me/museweaver/) is a live multi-agent code and mathematical verification studio powered by Meta Muse Spark Open (meta-models/muse-spark-open-1026 via Baseten). Single-pass code generation models frequently hallucinate subtle concurrency race conditions, distributed consensus split-brain vulnerabilities, and suboptimal dynamic programming recurrences that pass superficial unit tests. Instead of trusting a single completion, MuseWeaver orchestrates a 3-stage Proposer -> Adversarial Skeptic -> Formal Judge verification pipeline coupled with a deterministic in-browser JavaScript execution and property-based fuzzing sandbox. Across 3 built-in systems benchmarks (Lock-Free Token Bucket Rate Limiter, Byzantine Quorum Consensus 2f+1 vs 3f+1, and Battery Arbitrage Bellman DP) plus a live Custom Task Composer, MuseWeaver streams Muse Spark Open reasoning_content traces, extracts formal invariants, runs 1,000+ randomized fuzz trials in the browser to expose concrete counterexamples in naive implementations, and renders an interactive SVG Proof Dependency DAG with exportable Markdown/JSON verification certificates.