Formal Foundry

Proof-assistant-backed infrastructure for AI-assisted formalization.

Works — Tools for turning expert rules, operational data, and layered workflows into reviewable formal artifacts.
Case Studies — Applied formal verification across hardware, medical documentation, and coding-agent workflows.
Blog / Learn — Learning material on formalization, checked rulebooks, modeling choices, proof assistants, and evidence.
Book a Meeting — Start a scoped conversation about rulebooks, workflows, checked data, or formalization infrastructure.
Domains — Domain surfaces where rules, exceptions, thresholds, and obligations can be represented as checked artifacts.
Agda Libraries and Formalizations — Reusable Cubical Agda infrastructure, formal web artifacts, state-machine foundations, temporal logic, SMT tooling, implementation towers, and constructive mathematics.
News — News, events, academic collaborations and awards from FormalFoundry.
Papers — Research papers, technical reports, and working publications.

Homepage highlights

MLTTDB — A typed operational term-store system for proof-assistant workflows.
State Machine Studio — A modeling surface for hierarchical state machines and formalization workflows.
Codex Scribe — Expert-led formalization with AI assistance, Agda type checking, and deterministic readback of formal statements.
Sensitive medical documentation
Cauchy-complete real numbers, fully constructive as a HIT — TYPES 2026 work on constructive real analysis and algebraic foundations in Cubical Agda.
Formal Foundry Whitepaper — Our 2023 architecture whitepaper on AI and formal verification, revisited in 2026.
Implementation Towers — Agda formalization work around abstraction layers, implementations, observability, liveness, migration, instrumentation, runtime protocols, and control.
NextGen Sustainability 2026 — September 26, 2026
UR AI Summit 2026 — September 26, 2026
SpaceShield Summit 2026 — September 26, 2026
Milipol Innovation Award 2025 — September 26, 2026

info@formalfoundry.ai

2026

A Cubical Path from Algebra to Analysis

Open-source collaboration + Formal Foundry Research Group

Abstract—We connect algebraic interfaces to constructive analysis in Cubical Agda, tracing a path through ordered rings, premetric spaces, completions, continuity, and real-number infrastructure. The work demonstrates how informal mathematical intent can be decomposed into reusable checked components that support later high-stakes formalization work. It also shows how reusable real-number components can carry definitions across a larger development.

Index Terms—formal methods, proof assistants, verified systems, typed artifacts

2023

Formal Foundry Whitepaper

Formal Foundry Team

Abstract—A position paper on AI-assisted formalization where proof assistants remain the deterministic checking boundary. It frames AI as an accelerator for drafting, search, and translation, while formal definitions and checked proofs provide the audit trail needed for large-scale correctness in complex intelligent systems. The emphasis is not automation alone, but a reviewable boundary where generated candidates become trustworthy artifacts only after deterministic checking.

Index Terms—formal methods, proof assistants, verified systems, typed artifacts

2026

Implementation Towers

Formal Foundry Research Group

Abstract—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.

Index Terms—formal methods, proof assistants, verified systems, typed artifacts

Autonomy

invariants
protocols
fail states

Legal

definitions
jurisdiction
obligations

Clinical

contraindications
eligibility
safety rules

Tax

exemptions
nexus
credits

Code

specifications
proofs
regression constraints

Policy

eligibility
thresholds
public systems

MLTTDB

FSM Studio

Codex Scribe

NextGen Sustainability 2026

UR AI Summit 2026

SpaceShield Summit 2026

Milipol Innovation Award 2025

A Cubical Path from Algebra to Analysis

Formal Foundry Whitepaper

Implementation Towers

Autonomy

Legal

Clinical

Tax

Code

Policy

Implement post-quantum cryptography on hardware

Scale up sensitive medical documentation workflows

Create an unbreakable harness for coding agents

Proof-assistant-backed infrastructure for AI-assisted formalization.

Watch how

Proof-backed working surfaces

Reusable checked infrastructure

Rules under real constraints

Research records

Explanations and field notes

Explore Formal Foundry

Find a page