In CQL (http://categoricaldata.net), which generalizes relational theory with category theory, you can annotate schemas with equations and have them checked at runtime, or at compile time with an automated theorem prover (e.g., to establish that a query into a schema with a constraint will always materialize an instance that satisfies that constraint). One example is de-normalization: https://www.categoricaldata.net/denorm.php