24 tagged formal methods, measured the same way as everything else here.
Browse within: LaTeX 9beta 9z-notation 9z-notations 9ai-agent-tools 5behaviour-driven-development 5bounded-model-checking 5formal-specification 5invariants 5javascript 5model-checking 5python 5spec-driven-development 5
Agent
Generate tests from Allium specifications. Use when the user wants to propagate tests, generate test files from a spec, write tests for a specification, create property-based tests, produce state machine tests, check test coverage against spec obligations, or understand what tests a specification requires.
Agent
Tend the Allium garden. Use when the user wants to write, edit, update, add to, improve, clarify, refine, restructure, fix or migrate Allium specs. Covers adding entities, rules, triggers, surfaces and contracts, fixing syntax or validation errors, renaming or refactoring within specs, migrating specs to a new…
Agent
Weed the Allium garden. Find where Allium specifications and implementation code have diverged, and help resolve the divergences. Use when the user wants to check spec-code alignment, compare specs against implementation, audit for spec drift or violations, sync specs with code or code with specs, or verify whether…
Agent Claude Code
Use PROACTIVELY after changing Rust FSL syntax, lowering, semantics, CLI commands, public Kernel contracts, or corpus specs. Reports missing coupled code, tests, docs, skills, generated artifacts, and changelog updates. Read-only.
Agent Claude Code
Use PROACTIVELY after changing Rust core/runtime/verifier/solver/refinement semantics. Audits symbolic BMC versus the solver-independent Monitor/BFS, false-negative risk, dependency boundaries, and cross-implementation evidence. Read-only on source; may run focused tests.
Agent Claude Code
Use PROACTIVELY after adding or changing a .fsl spec under specs/ or examples/. Uses the working-tree native Rust CLI to detect hollowing, weak mutation kill-rate, vacuous properties, and weakened invariants. Read-only on specs; may run verifier commands.
Agent
Autonomously author NEW verifiable stateful code from a feature description — draft a contract, author a SAM v2 strict-profile module, self-repair against reachable invariant violations, synthesize a demo/regression corpus — and return the report. Use to generate a state machine, workflow, or reducer that comes out…
Agent
Autonomously prepare an invariant-elicitation session — harvest candidate invariants from the contract vocabulary, traces, and snapshots, pre-check each against the machine (HOLDS / counterexample / BOUNDED / ERROR), run the mutation adequacy grade, and return the ranked question list with evidence. The INTERVIEW…
Agent
Autonomously run the Polygraph verification loop (SAM v2 strict-profile artifact) given a contract, a source file, and a trace corpus. Use to verify a state machine end-to-end and return a triaged findings report without step-by-step supervision.
Agent Claude Code
Cognitive scientist and design theorist. Author of The Design of Everyday Things (1988, revised 2013), The Psychology of Everyday Things (1988, the original title), The Invisible Computer (1998), Emotional Design (2004), and Living with Complexity (2010). Co-founder with Jakob Nielsen of the Nielsen Norman Group…
Agent Claude Code
Python's creator and Benevolent Dictator For Life (1991–2018), now BDFL emeritus and a member of the Steering Council. Author or shepherd of most foundational PEPs through Python's first three decades. Currently focused on the faster-cpython project at Microsoft.
Agent Claude Code
Z notation specialist. Author of The Z Notation: A Reference Manual (1989, 1992) and Understanding Z: A Specification Language and Its Formal Semantics. Author of the fuzz type-checker that defines what valid Z really means. Oxford academic.