×

Agda Libraries and Formalizations

ff-json ff-generics ff-css ff-html ff-IEEE-754 ff-smt ff-owl ff-spartan6 semantic-explanation ff-generics-unsafe ff-html-examples ff-json-unsafe ff-owl-unsafe ff-smt-unsafe ff-spartan6-consumer-smoke ff-spartan6-tutorials ff-spartan6-unsafe semantic-explanation-integer-tutorial semantic-explanation-targets real numbers cubical-sm SMLogic tower

Formal Foundry’s library work is the engineering substrate behind the product pages. The stack uses proof assistants not only to check isolated theorems, but also to shape data interchange, generated interfaces, state-machine models, temporal claims, implementation layers, solver workflows, and constructive mathematics.

The main public project names are:

  • ff-json;
  • ff-generics;
  • ff-css;
  • ff-html;
  • ff-IEEE-754;
  • Cubical reals and constructive analysis.

The stack also includes companion libraries: cubical-sm for state-machine foundations, SMLogic for temporal logic over machines, tower for implementation layers, and ff-smt for SMT-LIB/Z3 workflows.

Read these pages as a map of reusable capabilities:

  • data transport and codec laws: ff-json;
  • typed datatype descriptions and editor generation: ff-generics;
  • typed web structures: ff-css and ff-html;
  • numerical representation foundations: ff-IEEE-754;
  • workflow and process semantics: cubical-sm and SMLogic;
  • implementation and runtime abstraction: tower;
  • solver-backed counterexample workflows: ff-smt;
  • deep mathematical credibility: Cubical reals and constructive analysis.

Generated HTML views, local servers, and public artifact pages are collected in Links and Artifacts.

Skip to content

Libraries

Agda Libraries and Formalizations

Reusable Cubical Agda infrastructure, formal web artifacts, state-machine foundations, temporal logic, SMT tooling, implementation towers, and constructive mathematics.

Formal Foundry’s library work is the engineering substrate behind the product pages. The stack uses proof assistants not only to check isolated theorems, but also to shape data interchange, generated interfaces, state-machine models, temporal claims, implementation layers, solver workflows, and constructive mathematics.

The main public project names are:

  • ff-json;
  • ff-generics;
  • ff-css;
  • ff-html;
  • ff-IEEE-754;
  • Cubical reals and constructive analysis.

The stack also includes companion libraries: cubical-sm for state-machine foundations, SMLogic for temporal logic over machines, tower for implementation layers, and ff-smt for SMT-LIB/Z3 workflows.

Read these pages as a map of reusable capabilities:

  • data transport and codec laws: ff-json;
  • typed datatype descriptions and editor generation: ff-generics;
  • typed web structures: ff-css and ff-html;
  • numerical representation foundations: ff-IEEE-754;
  • workflow and process semantics: cubical-sm and SMLogic;
  • implementation and runtime abstraction: tower;
  • solver-backed counterexample workflows: ff-smt;
  • deep mathematical credibility: Cubical reals and constructive analysis.

Generated HTML views, local servers, and public artifact pages are collected in Links and Artifacts.

Explore Agda Libraries and Formalizations

Libraries ff-json Cubical Agda infrastructure for JSON-like values, rendering, and codec laws. Libraries ff-generics Proof-carrying generic descriptions for finite datatype families, JSON codecs, and editor tooling. Libraries ff-css Typed CSS property declarations for checked HTML artifacts. Libraries ff-html Typed HTML trees, safe attribute renderers, selector evaluation, stylesheet matching, and generated examples. Libraries ff-IEEE-754 Cubical Agda foundations for IEEE-754 binary representation, decoding, finite-value semantics, and rounding … Libraries real numbers Research-grade Cubical Agda work from algebraic foundations toward real analysis. Libraries cubical-sm Cubical Agda foundations for state machines, homomorphisms, simulations, nested abstractions, and import/export … Libraries SMLogic Temporal logic over state-machine models: CTL*, LTL, CTL, evidence, fairness, checker boundaries, and trusted NuSMV … Libraries tower Cubical Agda formalization of implementation towers, runtime protocols, observability, liveness, migration, … Libraries ff-smt A safe Agda/Cubical SMT fragment with SMT-LIB rendering, Z3 counterexample workflows, and Agda-side refutation … Libraries ff-owl ff-owl formalizes the OWL 2 ontology language in Agda, covering raw syntax, checked and portable representations, … Libraries ff-spartan6 ff-spartan6 formalizes the construction, validation, and execution of digital designs for the Spartan-6 FPGA family. Libraries semantic-explanation semantic-explanation formalizes a domain-configurable route from reflected Agda terms to human-readable … Libraries ff-generics-unsafe ff-generics-unsafe provides an execution-enabled extension to generic programming over primitive atoms in Agda. Libraries ff-html-examples ff-html-examples is a compact Agda companion library that exercises typed HTML and CSS construction through … Libraries ff-json-unsafe ff-json-unsafe extends ff-json with compile-time integrations that execute external programs. Libraries ff-owl-unsafe ff-owl-unsafe is a compact integration layer for bringing external OBOGraph JSON into Agda while a module is being … Libraries ff-smt-unsafe ff-smt-unsafe is the execution-facing companion to ff-smt, coupling its formal SMT problem and statement … Libraries ff-spartan6-consumer-smoke ff-spartan6-consumer-smoke is a deliberately small downstream consumer that checks whether the public ff-spartan6 … Libraries ff-spartan6-tutorials ff-spartan6-tutorials is a sequence of eight Agda projects for learning verified digital-circuit construction in the … Libraries ff-spartan6-unsafe ff-spartan6-unsafe is the host-execution companion layer for generated JSON terms in the Spartan6 namespace. Libraries semantic-explanation-integer-tutorial The semantic-explanation-integer-tutorial library is a worked Agda tutorial that applies the semantic-explanation … Libraries semantic-explanation-targets semantic-explanation-targets is an integration library for attaching structured semantic explanations to logic, …
Book a meetingStart a scoped conversation

Cabinet index

Explore Formal Foundry

Book a meeting Explore libraries

Trusted systems. Mathematical proofs.

Search the archive

Find a page

Type to search the published content.