Papers
A framework for layered implementations with safe domains, observability, liveness, migration, and runtime protocol evidence. The formalization treats concrete systems as partial implementations of abstract ones, then asks which states, traces, controllers, and migration paths preserve the intended checked behavior. This makes architecture questions concrete: which states are safe, which arrows can run, and which migrations preserve evidence across layers.
Implementation towers are the strongest paper-style bridge between Formal Foundry’s product architecture and its Agda libraries.
The local tower library formalizes implementation layers over Cubical Agda categories. The key idea is that a concrete system may implement an abstract one only on a safe concrete domain. That domain, the interpretation into the abstract category, and the concrete category together form a partial implementation.
The tower formalization treats computations as categories:
Implementation is a partial interpretation functor;That gives a language for asking precise architecture questions. Can a concrete layer cover every abstract state? Can every needed abstract arrow be implemented between safe concrete endpoints? Does an observation recover a stable state? Does liveness provide a progress step? Can implementation layers compose?
The library then moves toward runtime-facing evidence:
RuntimeProtocol bundles completeness, observability, and liveness;The strongest examples are:
Implementation towers are the formal backbone for layered systems: a way to relate an abstract specification, a concrete implementation, runtime control, migration, and evidence without pretending that one flat proof covers everything.