Bibliography

Academic papers, books, and references cited across our PR/FAQ documents — collected from 195 citations across 10 repositories.

Journal Articles

article 2015 reason-trace

How Amazon Web Services uses formal methods

Chris Newcombe and Tim Rath and Fan Zhang and Bogdan Munteanu and Marc Brooker and Michael Deardeuff

Canonical reference for TLA+ in industry. AWS engineers used TLA+ to find subtle bugs in DynamoDB, S3, and other critical systems. Formal methods described as “surprisingly feasible” and “routinely applied” at Amazon scale.

article 1997 refactory

A refactoring tool for smalltalk

Don Roberts and John Brant and Ralph Johnson

The Refactoring Browser. Defines refactorings as provably correct parameterized transformations with preconditions guaranteeing behavior preservation.

article 2023 beadle

Use cases are essential

Ivar Jacobson and Alistair Cockburn

ACM peer-reviewed; argues for renewed use of use case methodology

article 2023 use-cases

Use cases are essential

Ivar Jacobson and Alistair Cockburn

Peer-reviewed ACM article calling for return to use case methodology. Jacobson invented use cases (1986 OOPSLA); Cockburn is co-author of Agile Manifesto. Published October/November 2023.

article 2009 z-spec

Formal methods: Practice and experience

Jim Woodcock and Peter Gorm Larsen and Juan Bicarregui and John Fitzgerald

Survey of 62 industrial FM projects: 92% reported quality increases, 0% reported decreases.

Conference Papers

inproceedings 2008 vox

The cost of interrupted work: More speed and stress

Gloria Mark and Daniela Gudith and Ulrich Klocke

Peer-reviewed. 36 knowledge workers. 23 min 15 sec average recovery time after interruption.  2 intervening tasks before returning to original work.

Books

book 1989 reason-trace

The Z notation: a reference manual

J. M. Spivey

The canonical reference for Z notation formal specification language. Z specifications describe state-machine behavior with mathematical precision. Used in safety-critical systems (railway signaling, nuclear, medical devices).

book 1999 refactory

Refactoring: Improving the design of existing code

Martin Fowler

The industry reference that popularized refactoring. Defines refactoring as “a change made to the internal structure of software to make it easier to understand and cheaper to modify without changing its observable behavior.”

Theses

phdthesis 1992 refactory

Refactoring object-oriented frameworks

William F. Opdyke

The originating PhD thesis establishing behavior-preserving program transformation as the formal definition of refactoring.

Reports

report 2025 quarry

State of AI code quality in 2025

Qodo

Developer survey: context pain affects 41–52% of developers by seniority; “improved contextual understanding” is the top-requested AI improvement (26% of votes); persistent context reduces frustration from 54% to 16%.

Standards

Miscellaneous

misc 2025 prfaq

Vibe coding

Andrej Karpathy

Original post coining the term “vibe coding” — viewed over 4.5 million times

misc 2026 vox

Measuring AI agent autonomy in practice

Anthropic

Primary data: median Claude Code turn  45 seconds; 99.9th percentile grew from ¡25 min to ¿45 min (Oct 2025–Jan 2026). Auto-approve rate grows from 20% for new users to 40%+ for experienced users (750+ sessions). Claude stops to ask clarification 2x more often than users interrupt on complex tasks.

misc 2026 vox

Hooks reference — claude code documentation

Anthropic

Official documentation of hook events: Stop (Claude finishes), Notification (permission_prompt, idle_prompt subtypes). Primary source for hook-based notification architecture.

misc 2019 dungeon

AI dungeon

Latitude

Pioneering LLM text adventure launched 2019; reached 100,000 players in first week and 1.5 million by June 2020; retired from Steam March 2024

misc 2026 use-cases

Autonomous agent system — use case development transcript

Punt Labs

Internal primary source. Transcript of a complete AI-guided use-case elicitation session using Jacobson-Cockburn v1.1. Produced 8 use cases (v1.0) in five iterative rounds with all open questions resolved. Existence proof that AI-guided methodology application is feasible.

misc 2025 z-spec

SysMoBench: Evaluating AI on formally modeling complex real-world systems

Qian Cheng and Ruize Tang and Emilie Ma and Finn Hackett and Peiyang He and Yiming Su and Ivan Beschastnikh and Yu Huang and Xiaoxing Ma and Tianyin Xu

LLMs handle small formal modeling artifacts; significant performance gaps remain for complex real-world distributed systems in TLA+.

misc 2025 z-spec

A benchmark for vericoding: formally verified program synthesis

Sergiu Bursuc and Theodore Ehrenborg and Shaowei Lin and Lacramioara Astefanoaei and Ionel Emilian Chiosa and Jure Kukovec and Alok Singh and Oliver Butterley and Adem Bizid and Quinn Dougherty and Miranda Zhao and Max Tan and Max Tegmark

LLM success rates: 82% Dafny, 44% Verus/Rust, 27% Lean. Dafny improved from 68% to 96% in one year.

misc 2025 prfaq

2025 developer survey

Stack Overflow

Annual survey of 65,000+ developers on tools, practices, and AI adoption

misc 2025 vox

TTS pricing comparison 2025

TextToLab

OpenAI TTS: $15/1M chars (tts-1), $30/1M chars (tts-1-hd). AWS Polly: $4.80/1M standard, $19.20/1M neural. ElevenLabs: subscription from $5/month / 30K chars.

misc 2024 beadle

RFC 9580: OpenPGP

Werner Koch and others

Current OpenPGP standard; July 2024; v6 formats, post-quantum ML-KEM keys

Online Resources

online 2025 reason-trace

AgentOps — Developer platform for AI agents

AgentOps

Product homepage. Confirms: Time Travel Debugging (session waterfall timeline), tool call tracking. Requires SDK instrumentation (2 lines of code). No terminal recording.

online 2026 reason-trace

The middle loop

Annie Vella

Study of 158 software engineers' AI usage patterns. Introduces “supervisory engineering work” as a new intermediate loop between inner (coding) and outer (planning) development cycles. Engineers spend increasing time reviewing, validating, and directing AI output rather than writing code directly.

online 2025 use-cases

anthropics/knowledge-work-plugins

Anthropic

Anthropic-maintained plugins for knowledge workers. Confirms methodology plugins are a recognized category.

online 2025 reason-trace

Automate workflows with hooks — Claude Code Docs

Anthropic

Official Claude Code hooks documentation. 14 lifecycle events including PostToolUse, Stop, PreCompact. Hook stdin payload includes session_id, transcript_path, tool_name, tool_input, tool_response.

online 2025 reason-trace

asciicast v3 — asciinema docs

asciinema

Format spec. Five event types: o, i, m, r, x. Marker events carry time + optional string label. Explicitly extensible.

online 2025 reason-trace

AI agents in production 2025

Cleanlab

Survey of 95 professionals with AI agents in production. Fewer than 1 in 3 teams satisfied with observability. 42% of regulated enterprises plan review controls. Observability called “the weakest layer.”

online 2025 use-cases

State of AI vs human code generation report

CodeRabbit

Analysis of 470 open-source pull requests. AI-generated code produces 1.7x more issues, 2.74x more XSS vulnerabilities. Published December 2025 via BusinessWire.

online 2025 reason-trace

Lean4: How the theorem prover works and why it's the new competitive edge in AI

Dhyey Mavani

VentureBeat guest post. Documents Lean4 adoption by OpenAI, Meta, Google DeepMind (AlphaProof), and Harmonic AI ($100M raised). Key framing: formal verification as a “safety net” for LLMs — each reasoning step translated to Lean4 and proof-checked. VeriBench benchmark: LLMs verify only 12% of code challenges in Lean4, but iterative agent approach reaches 60%.

online 2025 reason-trace

The state of observability in 2025

Grafana Labs

n=1,255 responses, collected Sep 2024–Jan 2025, analysis by Censuswide. Alert fatigue is the No. 1 obstacle to faster incident response, outpacing next response by almost 2:1. Average user manages 16 data sources; 5% manage over 100. Strongest independent source for the collection-without-action pattern in observability.

online 2024 beadle

ACP: Agent control plane

HumanLayer

Open-source agent scheduler with email as a human-approval channel for outer-loop agents

online 2024 use-cases

Use-case foundation v1.1

Ivar Jacobson and Alistair Cockburn

Primary methodology document. Defines system of interest, primary actor, goal, basic course, and extensions. Freely available.

online 2024 use-cases

Use-case foundation

Ivar Jacobson International

Active commercial and training ecosystem. Certifications and training materials available.

online 2024 use-cases

Use-case 3.0: The definitive guide

Ivar Jacobson International

2024 evolution of the methodology. Documents the incremental, story-driven approach. Confirms the methodology is actively maintained and evolving.

online 2026 reason-trace

Six problems of agentic engineering

Jeff Freeman

Punt Labs blog post. Maps the agentic engineering coordination landscape as six layers: (1) Intent & Trust, (2) Context & Memory, (3) Team Communication, (4) Project Tracking, (5) Agent Teams, (6) Agent-to-Agent protocols. Published on punt-labs.com.

online 2025 reason-trace

Trace Claude Code with Langfuse

Langfuse

Official integration guide. Captures via Stop hook: user inputs, assistant responses, tool invocations (inputs/outputs), session grouping, timing. Structured JSON traces and spans. Does not capture terminal ANSI output.

online 2026 beadle

OpenClaw agentic AI threat assessment

Palo Alto Networks Unit 42

Concluded OpenClaw maps to all 10 OWASP risks for agentic applications; lacks enforceable trust boundaries between untrusted inputs and high-privilege reasoning

online 2025 quarry

Claude Code reaches 115,000 developers, processes 195 million lines weekly

ppc.land

Reports figures disclosed by Deedy Das (Menlo Ventures) on July 6 2025 — NOT an official Anthropic release. 115,000 developers, 195M lines per week. Anthropic confirmed only “5.5x revenue increase” for July 2025. Use Anthropic Series G announcement for confirmed figures.

online 2025 beadle

Proton mail Bridge

Proton

Local IMAP/SMTP server; open-source Go; paid subscription required

online 2026 reason-trace

Introducing SageOx

SageOx

Primary source from SageOx. Confirms four-component product: Team Context, Ledger of Work, Ox CLI (context priming), Web App. CEO: Ajit Banerjee (ex-Hugging Face).

online 2024 beadle

AutoGPT

Significant Gravitas

182,000+ GitHub stars; autonomous AI agent framework with local deployment

online 2025 punt-kit

Celebrating five years of backstage

Spotify Engineering

3,000+ organizations; adoption stalls at under 10% in most non-Spotify orgs; requires dedicated full-time team

online 2026 dungeon

The AI vampire

Steve Yegge

Coined the term “AI vampire” to describe cognitive fatigue from AI-assisted coding; documents “Nap Attacks” and productivity limitations

online 2026 biff

Welcome to gas town

Steve Yegge

Maturity model with 8 levels of AI integration in development workflows. Argues teams progress through stages from basic completion to full agent orchestration. Complements Eledath's agentic engineering levels with a practitioner perspective.

online 2025 reason-trace

GitHub Copilot crosses 20 million all-time users

TechCrunch

Satya Nadella announced 20M on Microsoft earnings call July 30, 2025. TechCrunch notes this is “all-time users,” not active. Paid subscribers: approx. 1.3M Q1 2025, growing 30% QoQ.

online 2025 quarry

Meta acquires AI device startup Limitless

TechCrunch

Meta acquired Limitless (formerly Rewind) December 5 2025. Founded by Dan Siroker and Brett Bejcek. Raised $33M+ from Sam Altman, First Round, a16z, NEA. Team joins Meta Reality Labs.

online 2025 use-cases

Spec-driven development — technology radar

Thoughtworks

Thoughtworks Technology Radar entry. Identifies SDD as “one of the most important practices to emerge in 2025.” Cites 60–70% rework rate in low-maturity teams without specifications.

online 2025 use-cases

Vibe coding

Wikipedia contributors

Encyclopedia entry confirming vibe coding as a recognized cultural phenomenon in software development.

online 2024 dungeon

AI dungeon

Wikipedia Contributors

Historical overview of AI Dungeon's development, LLM transitions, and timeline