These two concepts work together really well.
Recently I have been experimenting with Json Schema as a way to formally describe an API. It lists all possible inputs that are accepted in a single document. Equivalent schema documents exist for other contracts.
A property test is a way of stating invariants about a system. You write tests that make assertions about the system that are always true for a range of inputs. The testing tool generates an increasingly complex input an runs a series of assertions reporting the simplest case that fails.
If you have a formal input specification the simplest property test you have is I can accept this input without rejecting the message. The contract document gives you a source for the generators.
By creating a generator based upon a specification document allows the tests to keep up with all possible inputs. This is the closest that you can get to a formal proof for system correctness without requiring a single typesystem (which in a distributed system may be impossible).
One thought on “Formal Schemas and Property Tests”
Hey Chris – somewhat related, https://preserves.dev/ might be worth looking at given your schema interests.