Grounding & Formal Methods

agent harnessThe agent harness — identity, missions, and traceable 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. Ethos also owns mission provenance: commits carry git trailers, so `git blame` walks from a line of code to the commit, the mission that authorized it, the dispatch prompt, and the per-tool-call audit trail — something like git blame with missions attached. Teams define roles with tool restrictions, anti-responsibilities, and safety constraints. 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
• Mission provenance — `git blame` a line to its commit, mission contract, dispatch prompt, and audit trail (reason-trace, now absorbed into Ethos)
• Teams and roles — collaboration graphs, anti-responsibilities, safety constraints
• MCP server covering identity, attributes, extensions, sessions, teams, roles, and missions
• Three integration surfaces — filesystem (zero dependency), CLI (hooks/scripts), MCP (structured)
• Session audit logging — one JSONL line per tool invocation
• Lifecycle hooks across session events, and preconditions that gate a tool call on a prior read having happened
• ethos ui — a localhost dashboard where clicking a line of code shows the agent, prompt, and audit trail behind it

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 meetings — four agentic personas debate weak spots, an autonomous hive mode reaches consensus without you, and completed meetings replay as a voiced debate
• Researcher agent pulls evidence from local research files, Quarry search, and the web, producing biblatex citations
• Cascading feedback engine traces effects across all sections
• Compiles to print-ready PDF via LaTeX, or exports to Word (.docx) via pandoc
• A full slash-command surface, including /prfaq:vote for a structured go/no-go decision and /prfaq:streamline to cut redundancy and marketing language
• /prfaq:externalize turns a merged CHANGELOG into a customer-facing press release

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 wraps two tools that predate it by decades: 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 — as a Claude Code plugin, a standalone CLI, or an MCP server for other agents.

• 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
• elaborate enriches a spec with narrative pulled from design docs
• Standalone CLI and MCP server (--no-plugin) for editors and agents other than Claude Code