Our Experience: Practical Applications of Formal Methods

At Formal Foundry, our projects demonstrate practical expertise in applying formal verification and proof assistants—especially Cubical Agda—to real-world engineering problems. Our experience spans foundational mathematical work, such as formalizing real numbers and developing automated solvers for complex categorical structures, to practical tools bridging natural language and formal specifications.

We’ve created robust infrastructure to simplify integrating proof assistants into modern software stacks, such as the Agda Server and automated refinement tools like the Agda Runtime. Collaborative industry projects, such as e-Orzecznik, illustrate our ability to apply formal verification directly to enhance software correctness and reliability.

Our current formalization of First-Class Implementations further underscores our capacity to precisely model complex software architectures, ensuring clarity and verifiable guarantees.

Explore our projects below to see detailed examples of our diverse, practical experience:

Real Number Formalization

Formalized real numbers using Cubical Agda based on constructions from Homotopy Type Theory (HoTT). We implemented Couch reals without additional axioms and demonstrated nontrivial results, such as proving that the exponential function is a group isomorphism between additive and multiplicative groups. This project showcases our capability in advanced mathematical formalizations relevant to verifying complex domain logic.

Category Theory Solver

Developed a robust solver in Cubical Agda capable of handling complex category-theoretical structures involving arbitrary categories and functors. This demonstrates our proficiency in formalizing and automating sophisticated mathematical reasoning, applicable to structuring verifiable workflows in real-world AI systems.

Presented Group Formalization

Formalized groups by presentations in Cubical Agda, enabling automatic generation of multiple representations, such as delooping as Higher Inductive Types (HITs). Additionally, we implemented optimizations for reasoning about groups in cubical settings. This approach illustrates our strength in encoding and simplifying intricate domain-specific formal reasoning tasks.

Agda Server

Built a web-service wrapper around the Agda compiler, streamlining large-scale, parallel typechecking in cloud environments. This simplifies integrating Agda into modern software stacks, highlighting our capability in creating practical infrastructure for deploying formal verification methods in industrial settings.

Agda Runtime

Created a system that automates iterative refinement from natural-language type descriptions into fully type-checked Agda code, leveraging large language models to clarify user intent and propose precise code snippets. Interactions are logged for transparency, enabling smooth integration of formal verification into everyday software engineering workflows.

e-Orzecznik (e-O)

An ongoing collaboration aimed at formally verifying and enhancing software workflows for occupational medicine. We identified key areas suitable for formalization, encoded them in Agda, and integrated formal verification into e-O’s development process. This demonstrates our ability to practically apply formal methods and proof assistants to significantly improve software reliability, efficiency, and correctness in real-world business applications.

FSM Formalization Workflow

Developed an interactive workflow enabling users to iteratively transform natural-language statements into formalized Agda types describing properties of Finite State Machines (FSMs). This showcases our experience bridging intuitive descriptions and formal specifications, directly supporting our services in formalizing business rules and regulatory compliance scenarios.

First-Class Implementations Formalization

In collaboration with François-René Rideau, we’re formalizing his influential paper “Reflection with First-Class Implementations” in Agda. This work develops a formal framework that models computations as categorical structures, facilitating reasoning about software behaviors and properties like observability and correctness. By encoding this approach in Agda, we’re demonstrating how formal methods can rigorously clarify complex architectural concepts, enabling precise guarantees and verifiable designs applicable to advanced reflective software systems and runtime environments.