Grounding & Formal Methods

Amazon's Working Backwards process, inside the terminal.

Generate, review, and stress-test Amazon Working Backwards documents with specialized agents, simulated review meetings, and compiled PDF output. See an example — the PR/FAQ for this tool, written by the tool itself.

• Complete PR/FAQ document generation — press release, FAQs, four-risks assessment, feature appendix
• Simulated review meeting with four agentic personas who debate weak spots
• Researcher agent integrates with Quarry for semantic search
• Cascading feedback engine traces effects across all sections
• Compiles to print-ready PDF via LaTeX

Formal Z specifications for stateful systems.

Z is a specification language grounded in set theory and first-order predicate logic, developed at Oxford and standardized as ISO 13568. A Z spec describes a system as states, invariants that constrain them, and operations that transition between them — catching entire classes of bugs mathematically, not just the inputs you happened to test. Z Spec makes two powerful tools approachable inside Claude Code: Spivey's fuzz type-checker and the ProB animator/model-checker from HHU Düsseldorf. Extract specs from existing code, generate code from specs, type-check, and model-check — without learning the toolchain.

• Bidirectional: code2model extracts specs, model2code generates implementations
• Type-checks with fuzz — Spivey's Z type-checker from Oxford
• Animates and model-checks with ProB — state-space exploration from HHU Düsseldorf
• Derives test cases from specs using TTF testing tactics
• Lux visualizations — interactive dashboards for model-check results and counter-example traces
• Lean 4 proof obligations, runtime contracts, and property-based oracle testing
• B-Method support: create, type-check, animate, and refine B machines

agent harness The agent harness — identity, missions, and structured delegation.

The harness that connects agents to their work. Persistent identity (personality, writing style, expertise) loads automatically every session. Typed mission contracts enforce write-set boundaries, bounded rounds, and frozen evaluators — with an append-only audit trail. Teams define roles with tool restrictions, anti-responsibilities, and safety constraints. Identity is the connection point; the harness is the whole system. Three integration surfaces (filesystem, CLI, MCP) so any tool reads identity state without taking a dependency.

• Persistent identity — personality, writing style, talents, roles, team graphs, channel bindings
• Typed mission contracts — write-set boundaries, frozen evaluators, bounded rounds, audit trails
• Teams and roles — collaboration graphs, anti-responsibilities, safety constraints
• MCP server with 10 tools — identity, attributes, extensions, sessions, teams, roles, missions
• Three integration surfaces — filesystem (zero dependency), CLI (hooks/scripts), MCP (structured)
• Session audit logging — one JSONL line per tool invocation