Have you looked at model-based testing? One way to think of it as property-based testing for stateful system, though that's underselling it a little. It's surprisingly easy to come up models/specs for most stateful systems, including CRUD apps.
The first is that some effect happens asynchronously, potentially interleaved with other operations. Whether a client observes completion by polling or by receiving an event from a message broker is orthogonal to the specification itself - the model looks essentially the same in both cases. The built-in test executor uses polling, but that's an execution strategy, not a specification construct.
If you have a trace containing both requests/responses and observed events, you can use the model to check that the trace conforms to the specification. In practice, it helps if the events can be localized to some interval in the execution (e.g. "this happened after A and before B"); otherwise the checker has to consider many more possible concurrent interleavings.
The conformance testing docs hint at how this can be done, but don't yet show an event-driven example. It's a good enough question that I'll write a dedicated doc page on it.
Property-based testing and model-based testing are closely related. Both ask the developer to state the expected behavior of a system (whether you call it a property, invariant, model, specification, or contract) and then validate that behavior over arbitrary inputs and arbitrary sequences of operations. Property-based testing frameworks also typically provide fuzzing and shrinking.
Where we felt there was a gap was in expressing rich stateful behavior: models involving non-determinism (e.g. a timeout where the write may or may not have committed), concurrency, and eventual asynchronous completion, and then checking that an observed execution trace conforms to that model. Accordant aims to make those kinds of specifications concise and readable.
Once you have such a model, it's possible to integrate it with the fuzzing and shrinking capabilities of existing property-based testing libraries. We'll have documentation on that integration soon.
Every API has a contract - the rules for how it should behave. You can't withdraw more than the balance. You can't delete a resource with active references. You can't re-create what already exists. But usually these rules are never written down in one place. Accordant lets you write the contract directly, as executable code. Not documentation that drifts, but code - if the implementation stops behaving according to the contract, you get immediate failures. Not only can you use the executable spec to validate _arbitrary_ scenarios, you can also use the spec - a first class construct - to mechanically explore the state space of a system and generate interesting test sequences. The docs above have examples.
Also worth calling out that we've used the framework to model a number of complex, distributed real-world systems: those involving async processes, concurrency, retries and crash consistency. These are non-trivial specs (and they pair quite well with techniques like deterministic simulation testing). Great care has been taken to ensure the specs remain readable and concise despite that richness of behavior. For those of you old timers who might be familiar with Spec#/SpecExplorer and NModel, this model-based testing library is a descendant of that line of work.
With the rise in AI-assisted software development, I feel we need richer ways of specifying and validating software and I feel quite excited and bullish about the possibilities here. There's a lot more to say on the topic - follow my twitter feed if interested in more updates ;)
Yes, I understand why you made these design decisions. And I also agree that sticking to JS/TS keeps things simple (for humans, and LLMs). I generally default to the s and s' way of specifying things (in a C# property-based testing framework I'm working on) but looking at how you approached things here gives me another angle to think about.
Bombadil takes a fresh approach to UI testing I haven't seen before: online monitoring through LTL formulas. Unlike model-checking (say by TLC), LTL formulas over here unfold in lock-step with the UI and allow users to express interesting temporal properties during testing.
The other intriguing aspect was how state is modeled (or rather, maybe not explicitly modeled?). A lot of the examples show the state extracted from the DOM and temporal properties indicating what the next (or eventual) state _should be_. If we want to look at the existing state (according to the model/spec) when predicting the next state (similar to how you can use s when specifying s' in TLA+), there seems to be no direct way to do that. It should of course be possible to capture the state at an earlier time in a closure and use it in a thunk at a later point, so it should be possible to work around this but that can be a little awkward, maybe. I'm working on a project in this space (primarily geared towards backend API model-based testing) and the state of the _real_ system isn't globally inspectable unlike a web page so took a different route over there. Having said that, this is a very interesting design choice that's very intriguing (in a good way).
We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.
Microsoft Azure Storage | Seattle, WA | Onsite or Remote (US only)
Our team in Azure Storage is working on applying automated reasoning and validation techniques to scalably generate hundreds of thousands of tests to check data integrity and durability issues, and scalably validate a combinatorial number of feature interactions to catch regressions and subtle bugs that only happen under rare conditions. As a Software Engineer in this team, not only will you get an opportunity to use tools to specify and check the integrity, correctness and performance guarantees of a large and critical Azure service, you will also get an opportunity to work on building and improving the tools themselves as well as learn about existing state-of-the-art tools in this space. The lessons you will learn will be broadly applicable to any distributed system and will help accelerate your growth as a disciplined and thoughtful distributed systems engineer.
Microsoft's mission is to empower every person and every organization on the planet to achieve more. As employees we come together with a growth mindset, innovate to empower others, and collaborate to realize our shared goals. Each day we build on our values of respect, integrity, and accountability to create a culture of inclusion where everyone can thrive at work and beyond.
The official job posting is not live yet, so please reach out to me directly at [email protected] and include "Automated Reasoning and Validation Position" in the subject.
My team used Coyote to test their distributed service against network race conditions. It requires a little bit of setup to ensure all components that typically run on separate machines can run in a single process, and inter-process communication happens through interfaces that can be stubbed out during testing.
I designed a series of workshops to teach these ideas internally at Microsoft. You can find the source code used in the workshop at https://github.com/microsoft/coyote-workshop - the repo can use better README files but sharing it nonetheless in case the setup helps inspire your own use of Coyote.
TLA+ and Coyote pair quite well actually. Verifying the high level design in TLA+ while checking subtle bugs as you translate that design to an implemention.
Check out Coyote (which is an evolution of P) and allows you to "model check" .NET code to find hard to find race condition-y bugs in your implementation. We have used it very successfully on a number of projects at Microsoft. I should probably do more public talks on it to get the word out. Finding subtle bugs in your implementation using tools like Coyote is easier than most people realize.
Coyote (concurrency exploration tool for .NET programs) can be used to do something "similar". My team often writes tests which set up focused concurrency between different APIs, the tests use Coyote to explore different ways that concurrency can unfold and write a strong set of assertions and invariants that must be true at the end. It's not TLA+ but it's still quite effective, very teachable as developers are already familiar with writing C# tests and helps catch safety and liveness bugs in our actual code base (as opposed to a model of it). It's not the same, by design, and does a decent job at finding concurrency and distributed system bugs.
Source: I've modeled a number of CRUD like and non-CRUD like systems through the Accordant framework (https://github.com/microsoft/accordant)