TESTING: Mojeek Labs | RAG Search

Here’s something we’ve been testing out; we thought some of you would like to try it.

It’s an experimental version so please account for that when using it. Any feedback is much appreciated

Answer generated by large language models, please double check for correctness. Search results provided by Mojeek. Projects on Mojeek Labs are experimental and liable to break or go down.

N.B. works in English, French, Italian, German and Spanish; will likely perform best in English currently.


I would put the Mojeek spell check up at the top like it is with regular search. I misspelled a word and Labs did okay with the text but some of the links were off.

I then intentionally did some searches with misspellings and then the correct spelling. On the misspelling the text seemed to give me an answer for the proper spelling however the text was totally different for the correct spelling.

Despite the spelling thing this is really interesting and has a lot of promise.


Obviously, the first thing I tried was Japanese text (e.g. 君の意味). It responded with, “Sorry, we might be overloaded, try again later.”

Currently it should work in English, French, Italian, German and Spanish, with a focus on English. Apologies, no Japanese as of yet :smile:

Well, I had to try :stuck_out_tongue:

The most common questions I want answered are usually:


But hey, it does tell me when Broken Flowers was released.

Incidentally, it does actually work if you mix English with it: Mojeek Labs | RAG Search

I even got it to respond in Japanese: Mojeek Labs | RAG Search

Kind of a weird response, but technically correct if you think about it.

I asked it a fairly complicated question about a very recent topic that a lot of people are confused about: Mojeek Labs | RAG Search

It did surprisingly well.

It seems to be pretty good.


It seems to do a good job.

Also, it looks like the URL entities are being double encoded: %2520 instead of %20

# Query
where can i find information on tla+


# Result

TLA+ is a specification language for concurrent systems, and you can find
information about it in several places.

One resource is Ron Pressler's blog series about TLA+, which provides an
introduction and history of the language 1.

Another source is the website for TEACHLEARNACHIEVE (TLA) LTD, which provides
information about the company and its use of TLA+ 2.

You can also find information about TLA+ on GitHub, where the TLA+Toolbox and
TLC model checker are hosted 3.

Additionally, there is an article from 2014 that describes the use of TLA+ in
an industrial environment, including its benefits and limitations 4.

TLA+ was introduced in 1999 and is based on the temporal logic of actions, as
described in 5.

The TLA+ Proof System, or TLAPS, is used to mechanically check proofs written
in TLA+ 5.

There are also tools for translating algorithms written in PlusCal into TLA+
models and running them through the model checker [citation:itation:7].

TLA+ is a large and complex language, with PlusCal built on top of it, and
there is a syntax cheatsheet available to help understand the symbols used in
the language 8.

TLA+ in Practice and Theory
1 - pron.github.io
2 - www.companieslist.co.uk
GitHub - tlaplus/tlaplus: TLC is a model checker
3 - github.com
Industrial Use of TLA+
4 - lamport.azurewebsites.net
TLA+ - Wikipedia
5 - en.wikipedia.org
Beyond the Toolbox — Learn TLA+
6 - learntla.com
TLA+ Helps Programmers Squash Bugs Before Coding -
7 - spectrum.ieee.org
An Introduction to TLA+ and Its Use in Parties —
8 - www.innoq.com

What is the first installment in Ron Pressler's blog series about TLA +?
What is the name of the Private Limited Company TEACHLEARNACHIEVE (TLA) LTD's
What is the GitHub repository for TLC, the model checker for TLA+?
What is the article that provides an excellent picture of TLA+ use in an
industrial environment?

1 Like

This is absolutely fantastic. No negative feedback so far, other than problems you get with all LLMs (like the occasional unhelpful or wrong answer).