Add comprehensive Inspect AI documentation to chapter 3

Completed TODO in book/02-dafny-and-inspect/03-ch3.md with detailed coverage of the
Inspect AI framework, its abstractions, and value proposition for verification agents.

Content additions:

1. Introduction and Context:
   - Positioned Inspect as batteries-included alternative to raw Anthropic SDK
   - Explained it was created by UK AI Security Institute in May 2024
   - Connected to upcoming dual implementation (Inspect vs rawdog) in chapter

2. Value Proposition Section:
   - Addressed fragmented evaluation practices problem
   - Listed core benefits: less boilerplate, free observability, reusable components, production-ready
   - Explained specific value for verification agents (tool-calling, logging, no manual loops)

3. Core Abstractions Deep Dive:
   - Tasks: Dataset + solver + scorer pattern with code example
   - Solvers: Composable evaluation logic, built-in solvers (generate, CoT, self_critique, etc.)
   - Explained automatic tool-calling loop - key differentiator from manual implementation
   - Scorers: Multiple approaches (exact match, model grading, custom logic)
   - Connected to DafnyBench: verifier as perfect deterministic scorer

4. Tools Section:
   - 5-step explanation of tool registration and execution flow
   - Example verify_dafny tool for DafnyBench
   - Coverage of MCP integrations, built-in tools, sandboxing capabilities

5. Metrics and Logging:
   - Automatic logging features (model calls, tool calls, states, timing)
   - inspect view web interface capabilities
   - Zero-infrastructure observability value prop

6. History and Ecosystem:
   - Timeline: May 2024 launch
   - inspect_evals repository collaboration (UK AISI, Arcadia Impact, Vector Institute)
   - Categorized major benchmarks: agent (GAIA, SWE-Bench), coding (HumanEval, BigCodeBench),
     cybersecurity (Cybench, CVEBench), knowledge/reasoning (GPQA, MMMU)
   - Positioned formal verification as emerging use case

7. When to Use Inspect:
   - Best use cases: agent evals, reproducible benchmarks, rapid iteration, production
   - When to avoid: need full control, non-LLM evals, minimal dependencies
   - Justified choice for DafnyBench implementation

Sources referenced:
- https://inspect.aisi.org.uk/ (official documentation)
- https://github.com/UKGovernmentBEIS/inspect_evals (community benchmarks)
- https://github.com/UKGovernmentBEIS/inspect_ai (main repository)

The documentation bridges DafnyBench theory (ch2) with practical implementation (ch4),
explaining abstractions while maintaining cookbook's educational voice. Includes note
that content needs human audit for tone and length.

Co-Authored-By: Claude <noreply@anthropic.com>

Author: quinn-dougherty