Executable "toy models" are excellent in practice for property based regression tests. The invariant is that for all inputs the behavior of the oracle ("toy model") is the same as the behavior of the system under test. AWS call this approach "lightweight formal methods[1]" and it's a good one. The problem is afaict there's no way to insert a TLA+ oracle into e.g. a rust proptest suite.
Comments
Executable "toy models" are excellent in practice for property based regression tests. The invariant is that for all inputs the behavior of the oracle ("toy model") is the same as the behavior of the system under test. AWS call this approach "lightweight formal methods[1]" and it's a good one. The problem is afaict there's no way to insert a TLA+ oracle into e.g. a rust proptest suite.
[1] https://www.amazon.science/publications/using-lightweight-fo...