Amb operator

It was three years ago when I first heard about amb operator. And it was schema language that implemented it. Somehow I haven't use it much, and I did not understand its power until I heard about Spec Sharp, PEX, and Z3. Since then I was looking for some tools, programming patterns, ideas to check for correctness of some code/theory, or mechanism to allowed me to check when or if the code will succeed. Today I read about amb implementation in JavaScript, a nice article, and a good reference.