tower is an Agda library for formalizing implementation towers over Cubical Agda categories.

It is the most architecture-oriented local library. It asks how a concrete system implements an abstract one, how safe concrete domains are selected, how observations and liveness are exposed, and how implementation layers compose.

Core View

The basic Implementation record represents an implementation of an abstract category by a concrete category as a partial functor. The partial domain is the full subcategory of concrete states satisfying Safe, so an implementation has the shape:

abstract category <- safe concrete domain -> concrete category

Soundness is not stored as a separate field. It is the functoriality of the interpretation functor. Completeness is split into object completeness, arrow completeness, strong completeness, operational complete-step, and weaker variants.

Runtime And Control

The library develops:

• Complete, Observable, Liveness, and RuntimeProtocol bundles;
• composeImplementation for implementation composition;
• implementation equivalence and composition laws;
• selection policies and stopping policies;
• scheduler policies with stop and continue branches;
• packed runtime decisions, stop decisions, continue decisions, and coherence proofs;
• protocol views with packed arrows, packed safe objects, endpoint checks, observations, complete steps, and liveness steps.

This is not just a mathematical exercise. It is a vocabulary for runtime-facing evidence: which concrete states are safe, how an abstract state is recovered, when progress is available, and how a controller decision relates back to the underlying implementation.

Migration And Instrumentation

The library also covers migration, semantic towers, and instrumentation:

• source stabilization followed by target object completeness;
• runnable migration steps;
• target-side liveness after migration;
• grounded state and arrow views over a shared lower computation;
• semantic-preserving path-control transitions;
• code instrumentation, repair, payload, tracing, logging, profiling, coverage, access-control, and concurrency-control aliases.

Examples

Two local examples are especially useful for site content:

• Tower.Examples.Nonlinear, a nonlinear finite work order with incomparable left-only and right-only states;
• Tower.Examples.PartialReplete, a partial/replete example where safe concrete states satisfy a visible invariant and unsafe intermediate states are repaired to safe points.

Use this page as the bridge between the “papers” section and product architecture. Towers explain how Formal Foundry thinks about layered systems, not only isolated proofs.

Most software systems live in layers. A high-level rule is implemented by a workflow. A workflow is implemented by data structures. Data structures are implemented by code. Code is executed by runtimes. At each level, someone wants to know whether the lower layer still means what the upper layer said.

tower gives that question a formal vocabulary. Not every concrete state has to be meaningful, but every safe concrete state has an abstract interpretation. Soundness is functoriality. Completeness, observability, liveness, migration, instrumentation, and runtime control then become explicit structures instead of informal architecture claims.

That makes tower a bridge between the formal libraries section and the papers section. It supports the company’s broader language of abstraction layers, runtime evidence, and controlled implementation without pretending that one flat proof covers every layer.