Skip to content

RosettaBitcoin: An Artifact-Backed Experience Report on Verification Infrastructure for Agent-Assisted Consensus Validators

Sep 2026 · 0 citations · 11 references
Computer Science

TL;DR

The case suggests that explicit failure records, fixtures, port-owned proofs, and validating imports can make agent-assisted systems more auditable and controlled ablations and external replications are needed to test whether such infrastructure causally improves development outcomes.

Abstract

Agent-assisted software projects are often reported through demonstrations or aggregate benchmarks that conceal how correctness claims were admitted. This experience report studies RosettaBitcoin, a single-developer project that built twelve separately implemented Bitcoin testnet4 consensus validators, through its immutable 17 June 2026 software snapshot (DOI 10.5281/zenodo.20738249). We analyze the snapshot's tracked SQLite evidence database, curated artifact index, conformance fixtures, validation scripts, blocker records, and version history. At the snapshot, all twelve ports had port-owned 45/45 script-corpus proofs and strict 5,000-block baselines. Nine had canonical clean 50,000-block, 100,000-block, and post-100,000 validation lanes. Java had one 19.86-second near-tip maintenance artifact. No port had an empty-state-to-tip proof, and no port satisfied the project's binary full-node gate; Docker and live-node capability gaps remained. The artifact history also records a 3 h 17 min 57 s Zig scaffold-to-50,000 span, but the observed intervals describe non-equivalent tasks and cannot estimate effort, productivity, or causality. A separate diagnostic supplement preserves evidence that a pure-Mojo cryptographic backend validated fresh state to height 100,000 and resumed to 140,234, agreed on a 45-case shadow comparison, rejected six crafted invalid classes, and was killed by three targeted mutations. That evidence is noncanonical, noncomparable, and class-bounded. The case suggests that explicit failure records, fixtures, port-owned proofs, and validating imports can make agent-assisted systems more auditable. Controlled ablations and external replications are needed to test whether such infrastructure causally improves development outcomes.

View source

Similar papers

Preprint Aug 2026

CAPRI: Contract-Aware Proof Repair for Isabelle

CAPRI is presented, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract, in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract.

Jim Woodcock, Gabriel Leite, Augusto Sampaio et al. · 1 citation
Preprint Aug 2026

Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study

CAPRI, a contract-aware proof-repair tool, is used to govern a reconstruction by combining Isabelle acceptance with an independent check of repository changes against machine-readable edit contracts, and the reconstruction discharged all ten scoped obligations within the original nine-theory structure.

Jim Woodcock, Gabriel Leite, Augusto Sampaio et al. · 0 citations

Markdown Mayhem : Taming the Agentic Documentation Explosion

It is argued that without principled governance, agent-oriented documentation risks undermining both human comprehension and agent reliability, and a proposed foundational directions for restoring coherence are proposed.

Harsha Kokel · 0 citations
Review Sep 2026

Tracekit: Tamper-Evident Intent-Reasoning-Action Auditing for Autonomous Coding Agents

Autonomous coding agents read untrusted files, run shell commands and spawn sub-agents with little supervision, yet their record is usually an editable log. We present Tracekit, an open-source, dependency-free system that captures three channels for every agent session: what the human asked (intent), what the model sai...

Bravish Ghosh · 0 citations

Related blog posts

MIT News · Artificial Intelligence Oct 2, 2026

Documenting the tech worker movement

Writing as a participant and researcher, PhD student JS Tan SM ’22 has co-authored a new book about the rise of tech worker protests and the employer backlash that followed.

GPT-Lab Sep 23, 2026

Requirements Don’t Live in Isolation: What We’re Exploring with Req-Space

Requirements in large systems rarely exist in isolation. Their meaning depends on the wider project context - other requirements, policies, decisions, tests, and implementation details. That becomes especially important when AI is used for review, because spotting a possible conflict or gap is only the beginning. ReqSpace explores how AI, visualisation, and connected project context can help reviewers understand those findings, trace the relationships behind them, and focus on the questions that…

GPT-Lab Sep 17, 2026

Beyond Prompt Engineering: The Role of Tacit Knowledge in Software Engineering

AI is making software generation faster, but speed does not remove the need for expertise. As more work is delegated to AI, tacit knowledge may become one of the most important human advantages in software engineering. The post Beyond Prompt Engineering: The Role of Tacit Knowledge in Software Engineering appeared first on GPT-Lab.

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.