Compass began as a workflow for formal modeling before implementation.
The core idea was to encode a system's high-level architecture as a checked, compiled specification: the same pattern I had used for security-relevant systems and algorithms that needed proof or validation before implementation. I originally used Lean for this, but Compass uses Agda because its tooling fits this workflow well.
In practice, I would first reason about changes in the compiled-spec layer, then use an agent to propagate those validated architectural changes through the implementation with a mostly hands-off workflow.
The results were promising enough that I decided to create Compass, which should be an environment for enforcing that workflow in agentic and agent-orchestrated software development.
Stepping back, the workflow worked because it gave agents three things:
- Reduced probabilistic gravity
- Lossless compression of the architecture
- The ability to modify the architecture itself in a "compiled" sense before modifying implementation code
Agents should navigate software through concepts, not files.
Important
Installation instructions are in INSTALL.md.
Compass is a concept-first workspace for AI agents.
Instead of exposing a repository as a hierarchy of files and folders, Compass exposes a repository as a collection of architectural concepts.
The filesystem becomes an implementation detail.
The architectural model becomes the primary interface.
Compass is not a formal verification framework.
It is a semantic operating system that enables AI agents to reason, navigate and evolve software through architectural intent rather than implementation artifacts.
Its goals are:
- Global architectural alignment
- Context compression
- Controlled execution
- Architecture-aware navigation
Current coding agents operate roughly like this:
Repository
↓
Search
↓
Files
↓
Edit
This works remarkably well for localized modifications.
It performs much worse when modifications require architectural evolution.
When placed inside sufficiently large repositories, agents experience what Compass calls probabilistic gravity.
Probabilistic gravity is the tendency of language models to preserve existing implementation structures because those structures dominate the available context.
Rather than questioning architecture, agents naturally converge toward additive solutions.
Typical symptoms include:
- Bolting new paradigms onto old architectures
- Preserving accidental complexity
- Overlooking global assumptions
- Accumulating architectural drift
- Spending enormous token budgets exploring irrelevant implementation
Compass changes both the abstraction and the psychology.
Repository
↓
Architectural Concept
↓
Human Specification
↓
Formal Model
↓
Implementation
↓
Edit
Instead of beginning with implementation, every change begins with architectural intent.
Agents do not search repositories.
Agents select concepts.
Examples:
- Transaction Validity
- Ledger Consistency
- Search Ranking
- Authorization
- Media Timeline
Every architectural concept becomes a semantic entry point into the implementation.
Compass uses languages such as Agda or Lean.
However, formal verification is not the primary objective.
The formal model acts as a lossless executable compression algorithm for architectural intent.
"Lossless" is scoped to architectural meaning: invariants, obligations, trust boundaries, terminology, assumptions, and relationships that an agent must preserve. It is not a requirement to mirror every helper function, local formatting decision, test harness detail, or incidental implementation mechanism.
Instead of reading
150,000 lines of implementation
the agent reasons over
1,000 lines of dense mathematical structure
The model captures
- invariants
- terminology
- assumptions
- architectural relationships
- constraints
- obligations imposed on agents and maintainers
The implementation then becomes an expansion of this compressed representation. Supportive implementation details remain evidence or classified detail unless promoting them would change architectural reasoning.
Every implementation change must first pass through an architectural representation.
Compass enforces a guarded phase flow:
idle
↓
architecture-review
↓
implementation-open
↓
alignment-checked
During architecture-review, agents may update the specification/formal model if the change requires it, but ordinary implementation work remains blocked. The architecture checkpoint is the transition into implementation-open, where the normal toolchain is restored. Compass captures a baseline at begin_change, persists workflow state under .compass/.runtime, and computes touched-file/semantic alignment evidence at finish_change. The implementation is never the starting point.
A harness's Compass-mode activation is orthogonal to that persisted repository workflow. Turning a client integration off must restore its exact prior tool surface and contribute no Compass-owned tools or prompt guidance to subsequent agent requests; it does not rewrite or abort the repository workflow held by MCP. Re-enabling may therefore resume an in-progress guarded change without allowing disabled-mode policy to leak into unrelated work.
Compass calls an implementation faithful only when it starts from the checked model, records a representability verdict, rejects semantic-fraud shortcuts, and is aligned against Compass-owned baseline evidence. The architecture checkpoint establishes the preconditions for faithful implementation; the finish/alignment step checks whether the resulting work stayed faithful.
Compass models must also identify load-bearing abstractions: current semantic shapes that future implementation must preserve, extend, or explicitly replace. compass check fails when a model has no load-bearing abstractions, because concepts and bindings alone do not tell an agent what would make a local patch architecturally dishonest.
Compass avoids large manually maintained configuration files.
Instead, concept bindings live in the repository's checked Compass model.
Every accepted implementation change contributes evidence that the architecture model should evolve, but the semantic graph is not learned as an unconstrained telemetry database.
The architecting agent must express bindings through the Compass DSL using value-level ConceptEntry and RegionEntry declarations. Agda typechecks the authored architectural values and propositions, while Compass tooling handles registry hygiene such as duplicate keys and graph extraction. Code classifications are concept-free accounting roles stored directly on registered regions, each backed by non-empty evidence.
Do not invent concepts for miscellany. Known regions that do not carry architectural meaning should be registered only when they need semantic accounting, then classified as implementation detail, generated code, external code, or explicitly unclassified follow-up. Unlisted implementation is outside the current semantic frontier; agents should treat it as support/evidence rather than infer new architecture from it until a model update promotes it.
Example evidence:
Strong evidence
- implementation modified while operating under concept
- human accepted pull request
- concept-specific checks passed
Medium evidence
- dependency graph relationship
- repeated implementation changes
Weak evidence
- implementation inspected
- implementation referenced
Bindings carry supporting evidence from the checked model rather than metadata maintained in a disconnected graph.
Over time Compass evolves the formal semantic structure of the repository.
Compass separates software reasoning into three layers.
Human Specification
Written for humans.
Example
Transactions must not occur before account creation.
Accepted transactions always create ledger entries.
Overdrafts require explicit authorization.
Architects primarily edit this layer.
Formal Model
Implemented using Agda or Lean.
Purpose:
- executable specification
- architectural compression
- theorem support where desired
- machine-readable invariants
The formal model is primarily consumed and edited by AI, but if you understand Lean, you can take your shot.
It should be lossless over architectural obligations, not exhaustive over implementation mechanics. A fact belongs in the formal model when changing or omitting it could cause an agent to misunderstand the system's semantic structure, trust boundary, or evolution rules.
Semantic Binding Graph
Compass exposes a continuously evolving semantic graph.
The graph is not the primary authored artifact. It is derived from the approved Compass model after Agda has checked that model.
The approved model contains the architectural facts and evidence; the graph is the runtime projection used by agents and MCP tools.
Nodes include
- concepts
- modules
- files
- functions
- APIs
Edges contain
- supporting evidence
- dependency information
- implementation bindings
- code classifications
The graph becomes the repository's semantic memory because it is projected from the checked source of truth.
Compass internally reasons over three interconnected graphs.
Represents architectural concepts and their relationships.
Authorization
↓
Authentication
↓
Session Management
Represents implementation dependencies.
Examples
- imports
- function calls
- module dependencies
- ownership
- package relationships
Bridges concepts to implementation.
Every concept-to-region binding stores non-empty supporting evidence.
Transaction Validity
↓
src/transactions/*
↓
ledger/apply.ts
The Binding Graph is continuously refined through accepted architectural evolution, but refinement happens by updating the checked Compass model. The graph itself is regenerated from that model.
Compass intentionally separates architecture from execution.
Execution is pluggable.
Possible execution strategies include
- single coding agent
- sequential workflow
- multi-agent orchestration
- human-assisted execution
Execution is not Compass itself.
Compass provides the semantic workspace.
One possible execution strategy.
Architect Agent
↓
Updates specification
↓
Updates checked Compass model
↓
Defines contracts and graph-relevant architectural facts through the DSL
↓
Concept-scoped reviewers inspect changes
↓
Intent plans generated
↓
Consensus reached
Once consensus exists
↓
Agents receive concept-scoped write access
↓
Implementation proceeds independently
Merger Agent validates
- interfaces
- invariants
- integration
- final pull request
Compass itself remains execution-agnostic.
Intent plans capture architectural reasoning before implementation.
Example
Concept
↓
Planned modifications
↓
Expected invariants
↓
Files likely affected
↓
Validation strategy
Once accepted, intent plans become permanent repository artifacts.
.compass/intents/
Future humans and agents can understand
- why a migration happened
- what assumptions existed
- what alternatives were rejected
Intent therefore becomes a first-class artifact alongside
- implementation
- specification
- architecture
Compass's central design principle.
Every architectural change must pass through a narrow conceptual gateway.
Instead of
Agent
↓
Entire Repository
Compass enforces
Agent
↓
Concept
↓
Human Specification
↓
Formal Model
↓
Intent Plan
↓
Bound Implementation
↓
Edit
Compass exposes semantic tooling rather than filesystem tooling.
Current MCP tools:
compass.graph_summary()
compass.list_concepts()
compass.list_dependencies()
compass.list_bindings()
compass.list_classifications()
compass.list_obligations()
compass.obligations_for_concept(concept)
compass.inspect_obligation(obligation)
compass.inspect_concept(concept)
compass.regions_for_concept(concept)
compass.concepts_for_region(region)
compass.dependency_neighborhood(concept)
compass.context_for_region(region)
compass.context_for_file(path)
compass.read_file(path)
compass.read_region(region)
compass.begin_change(intent, concepts?)
compass.record_architecture_checkpoint(summary, witness?)
compass.finish_change(summary)
compass.workflow_status()
compass.abort_change(reason)
compass.authorize_tool_call(toolName, input)
compass check is the canonical CLI validation command for humans, agents, and CI. It uses the same checked projection path as compass graph, compass explain, and compass mcp: Agda checks .compass/Compass.agda, Compass normalizes semanticModelFrom compassModel, and Compass then runs semantic model hygiene checks. The command exits nonzero for any finding, including unregistered dependency concepts, unregistered binding regions, duplicate pressure keys, missing load-bearing abstractions, invalid anchors, isolated concepts, unbound architectural regions, or other weak architectural pressure.
compass explain emits deterministic Markdown to stdout from the checked SemanticModel. It is a human-readable projection of what exists in .compass/Compass.agda, not an authored architecture document and not a managed workspace artifact. Redirect it to a file if you want to track the rendered view.
compass.record_architecture_checkpoint revalidates the checked model and derives both the representability assessment and reviewed/deferred obligation accounting from the typechecked Agda checkpoint witness. The witness must answer whether the current formal model can express the requested feature without lying (represented, extension, modelBreaking, or unknownRepresentability) and include a semantic fraud audit. unknownRepresentability blocks implementation; modelBreaking blocks implementation unless the Compass model changed during architecture review. Obligations attached to the explicit begin_change concepts or inferred from touched Compass regions must still be reviewed or explicitly deferred inside that witness. When obligations are missing, Compass returns a suggestedWitness scaffold derived from checked Agda obligation definitions to help the next checkpoint attempt.
compass.context_for_file and compass.context_for_region return compact contextBlock strings designed for harnesses to prepend to ordinary reads in a Compass-aware mode. compass.read_file and compass.read_region return that semantic context together with source text, allowing a locked-down agent harness to disable native filesystem read tools.
The filesystem becomes an implementation backend rather than the agent's primary interface.
CLI
compass init
compass check
compass explain
compass graph
compass mcp
Formal source of truth
- Agda-checked
.compass/Compass.agda compass initinstalls the reusable Agda framework modules.compass/Compass/Core.agdaand.compass/Compass/DSL.agda, plus a typechecking seedCompass.agdamodel and.compass/compass-workspace.agda-lib.
Agent integration
- Agents and humans propose model edits externally.
- Compass validates the checked model and serves semantic navigation plus guarded workflow tools over MCP.
- Pi and other harnesses integrate as MCP clients, not Compass-specific backends.
Compass gradually evolves a repository into a semantic operating system.
Instead of understanding software through
Folders
↓
Files
↓
Functions
agents should understand software through
Concepts
↓
Specifications
↓
Models
↓
Intent
↓
Implementation
The repository eventually develops an executable semantic memory.
Compass continuously compresses and refines this memory by updating the checked architecture model and regenerating the semantic graph from it as software evolves.
Compass gives AI agents a concept-first view of software, replacing file-centric navigation with semantic architectural reasoning while dramatically reducing the context required to safely evolve complex systems.