In this post I’ll share the results from testing TodoMVC implementations using my new testing tool named WebCheck. I’ll explain how the specification works, what problems were found in the TodoMVC implementations, and what this means for my project.


During the last three months I’ve used my spare time to build WebCheck. It’s a browser testing framework combining ideas from:

  • property-based testing (PBT)
  • TLA+ and linear temporal logic
  • functional programming

In WebCheck, you write a specification for your web application, instead of manually writing test cases. The specification describes the intended behavior as a finite-state machine and invariants, using logic formulae written in a language inspired by the temporal logic of actions (PDF) from TLA+. WebCheck generates hundreds or thousands of tests and runs them to verify if your application is accepted by the specification.

The tests generated by WebCheck are sequences of possible actions, determined from the current state of the DOM at the time of each action. You can think of WebCheck as exploring the state space automatically, based on DOM introspection. It can find user behaviors and problems that we, the biased and lazy humans, are unlikely to think of and to write tests for. Our job is instead to think about the requirements and to improve the specification over time.

Specifications vs Models

In property-based testing, when testing state machines using models, the model should capture the essential complexity of the system under test (SUT). It needs to be functionally complete to be a useful oracle. For a system that is conceptually simple, e.g. a key-value database engine, this is not a problem. But for a system that is inherently complex, e.g. a business application with a big pile of rules, a useful model tends to grow as complex as the system itself.

In WebCheck, the specification is not like such a model. You don’t have to implement a complete functional model of your system. You can leave out details and specify only the most important aspects of your application. As an example, I wrote a specification that states that “there should at no time be more than one spinner on a page”, and nothing else. Again, this is possible to specify in PBT in general, but not with model-based PBT, from what I’ve seen.

TodoMVC as a Benchmark

Since the start of this project, I’ve used the TodoMVC implementations as a benchmark of WebCheck, and developed a general specification for TodoMVC implementations. The TodoMVC contribution documentation has a high-level feature specification, and the project has a Cypress test suite, but I was curious if I could find anything new using WebCheck.

Early on, checking the mainstream framework implementations, I found that both the Angular and Mithril implementations were rejected by my specification, and I submitted an issue in the TodoMVC issue tracker. Invigorated by the initial success, I decided to check the remaining implementations and gradually improve my specification.

I’ve generalized the specification to work on nearly all the implementations listed on the TodoMVC website. Some of them use the old markup, which uses IDs instead of classes for most elements, so I had to support both variants.

The Specification

Before looking at the tests results, you might want to have a look at the WebCheck specification that I’ve published as a gist:


The gist includes a brief introduction to the WebCheck specification language and how to write specifications. I’ll write proper documentation for the specification language eventually, but this can give you a taste of how it works, at least. I’ve excluded support for the old TodoMVC markup to keep the specification as simple as possible.

The specification doesn’t cover all features of TodoMVC yet. Most notably, it leaves out the editing mode entirely. Further, it doesn’t cover the usage of local storage in TodoMVC, and local storage is disabled in WebCheck for now.

I might refine the specification later, but I think I’ve found enough to motivate using WebCheck on TodoMVC applications. Further, this is likely how WebCheck would be used in other projects. You specify some things and you leave out others.

The astute reader might have noticed that the specification language looks like PureScript. And it pretty much is PureScript, with some WebCheck-specific additions for temporal modalities and DOM queries. I decided not to write a custom DSL, and instead write a PureScript interpreter. That way, specification authors can use the tools and packages from the PureScript ecosystem. It works great so far!

Test Results

Below are the test results from running WebCheck and my TodoMVC specification on the examples listed on the TodoMVC website. I’ll use short descriptions of the problems (some of which are recurring), and explain in more detail further down.

Example Problems/Notes
Pure JavaScript
  • Clears input field on filter change
  • Clears input field on filter change
Compiled to JavaScript
Kotlin + React
  • Race condition on initialization
  • Filters not implemented
TypeScript + Backbone.js
TypeScript + AngularJS
TypeScript + React
Scala.js + React
Scala.js + Binding.scala
Humble + GopherJS
  • Missing/broken link
Under evaluation by TodoMVC
Backbone.js + RequireJS
KnockoutJS + RequireJS
  • Inconsistent first render
AngularJS + RequireJS
  • Needs a custom readyWhen condition
CanJS + RequireJS
Lavaca + RequireJS
  • Clears input field on filter change
  • Race condition on initialization
  • Filters not implemented
  • Missing/broken link
  • Clears input field on filter change
Kendo UI
  • Filters not implemented
Enyo + Backbone.js
  • No input field
React + Alt
React + Backbone.js
Angular 2.0
  • Filters not implemented
  • State cannot be cleared
Firebase + AngularJS
Express + gcloud-node
  • Missing/broken link
Non-framework implementations
  • Adds pending item on other interaction
VanillaJS ES6
  • Adds pending item on other interaction
  • .todo-count strong is missing
✓ Passed, ❌ Failed, – Not testable
Filters not implemented

There’s no way of switching between “All”, “Active”, and “Completed” items. This is specified in the TodoMVC documentation under Routing.

Race condition during initialization

The event listeners are attached some time after the .new-todo form is rendered. Although unlikely, if you’re quick enough you can focus the input, press Return, and post the form. This will navigate the user agent to the same page but with a query parameter, e.g. index.html?text=. In TodoMVC it’s not the end of the world, but there are systems where you do not want this to happen.

Inconsistent first render

The application briefly shows an inconsistent view, then renders the valid initial state. KnockoutJS + RequireJS shows an empty list items and “0 left” in the bottom, even though the footer should be hidden when there are no items.

Needs a custom readyWhen condition

The specification awaits an element matching .todoapp (or #todoapp for the old markup) in the DOM before taking any action. In this case, the implementation needs a modified specification that instead awaits a framework-specific class, e.g. .ng-scope. This is an inconvenience in testing the implementation using WebCheck, rather than an error.

No input field

There’s no input field to enter TODO items in. I’d argue this defeats the purpose of a TODO list application, and it’s indeed specified in the official documentation.

Adds pending item on other interaction

When there’s a pending item in the input field, and another action is taken (toggle all, change filter, etc), the pending item is submitted automatically without a Return key press.

.todo-count strong element is missing

An element matching the selector .todo-count strong must be present in the DOM when there are items, showing the number of active items, as described in the TodoMVC documentation.

State cannot be cleared

This is not an implementation error, but an issue where the test implementation makes it hard to perform repeated isolated testing. State cannot (to my knowledge) be cleared between tests, and so isolation is broken. This points to a key requirement currently placed by WebCheck: the SUT must be stateless, with respect to a new private browser window. In future versions of WebCheck, I’ll add hooks to let the tester clear the system state before each test is run.

Missing/broken link

The listed implementation seems to be moved or decommissioned.

Note that I can’t decide which of these problems are bugs. That’s up to the TodoMVC project maintainers. I see them as problems, or disagreements, between the implementations and my specification. A good chunk of humility is in order when testing systems designed and built by others.

The Future is Bright

I’m happy with how effective WebCheck has been so far, after only a few months of spare-time prototyping. Hopefully, I’ll have something more polished that I can make available soon. An open source tool that you can run yourself, a SaaS version with a subscription model, or maybe both. When that time comes, maybe WebCheck can be part of the TodoMVC project’s testing. And perhaps in your project?

If you’re interested in WebCheck, please sign up for the newsletter. I’ll post regular project updates, and definitely no spam. You can also follow me on Twitter.


If you have any comments or questions, please reply to any of the following threads:

Thanks to Hillel Wayne, Felix Holmgren, Martin Janiczek, Tom Harding, and Martin Clausen for reviewing drafts of this post.