Tools shelf ยท 19 runnable tools
Tools where code keeps the model honest
The library lists research systems. This shelf lists software you can install today, in which an algorithm computed in code (a grammar, a validator, a test run, an evaluator, a proof kernel) judges or steers what a model proposes. Each entry has an install line and a plain statement of what it does not prove.
What gets on the shelf
- It is open source, with a public repository and a stated license.
- You can run it: it has an install line in its own documentation.
- An algorithm computed in code judges or steers the model. A prompt-only skill or a second model acting as judge does not count.
- Every entry was checked against its repository and README on the date shown.
These are not research systems and are not in the library's count. Under this library's definition, many of them are building blocks and some are full loops; corrections are welcome. None of the listed projects is affiliated with this library, and none of them is claimed to use the term AlgoGen.
Know a tool that fits? Submit your system or tool. Entries are checked against their repository before they go on the shelf.
- Code-run loopMIT
Agentless
Fixes software issues in three fixed steps (locate, repair, validate) and ranks candidate patches by test results.
- Proposes
- Several candidate patches per issue
- Judged by
- Regression tests it selects plus reproduction tests, run in code
- Steers
- Test results re-rank the patches and the best one is submitted
Install
git clone https://github.com/OpenAutoCoder/Agentless && cd Agentless && pip install -r requirements.txtWhat it does not prove: Passing the selected tests does not show the patch is correct or complete. The reproduction tests are themselves written by the model, so they can miss the real bug. Setup also needs an OpenAI API key.
- ToolApache-2.0
Aider
A terminal coding assistant that runs your linter and test command after each edit and asks the model to fix failures.
- Proposes
- Code edits to your repo
- Judged by
- Your lint command and test command (non-zero exit code means failure)
- Steers
- Failure output is fed back so the model repairs the edit
Install
python -m pip install aider-install && aider-installWhat it does not prove: A clean lint and test run shows only that those checks pass. Behavior the tests do not cover is unchecked, and the tests are only as good as you made them.
Aider READMEAider docs: Linting and testingAider repoChecked
- Code-run loopApache-2.0
CodeEvolve
Open-source evolutionary coding agent: LLMs rewrite code, sandboxed evaluation scores it, islands and an archive steer.
- Proposes
- LLM-written code variants
- Judged by
- sandboxed execution of the candidate with fitness extracted from the evaluation results
- Steers
- island-based genetic algorithm with migration, plus an optional MAP-Elites archive, selects parents
Install
git clone https://github.com/inter-co/science-codeevolve.git && cd science-codeevolve && conda env create -f environment.ymlWhat it does not prove: A fitness number shows a candidate does well under the given evaluator, not that it is the best solution or that the evaluator is complete.
CodeEvolve READMEChecked
- LibraryMIT
DSPy
Python framework whose optimizers (MIPROv2, GEPA and others) tune prompts and weights to maximize a metric you write.
- Proposes
- candidate instructions and few-shot examples for each module
- Judged by
- a metric function you write that scores program outputs
- Steers
- optimizers such as MIPROv2 (Bayesian search) and COPRO (hill-climbing) keep the settings that raise the metric
Install
pip install dspyWhat it does not prove: A prompt tuned on a metric and a training set is only as good as that metric; gains may not carry to new inputs or to what the metric misses.
- LibraryApache-2.0
Guardrails AI
Python framework that runs validators on LLM inputs and outputs and decides what to do when a check fails.
- Proposes
- an LLM response, or a user input headed to the model
- Judged by
- validators in an input or output Guard, such as RegexMatch, plus custom validators you write
- Steers
- each validator has an on_fail action, for example raising an exception, which blocks or redirects the output
Install
pip install guardrails-aiWhat it does not prove: A validator only proves the one property it checks. Some hub validators (for example toxic-language checks) are themselves model-based, so they are not pure code judges.
- LibraryMIT
Guidance
Python library that steers a model while it writes, using regex, choice lists and grammars to constrain each generated piece.
- Proposes
- text for each gen() slot in a program, from Transformers, llama.cpp or other backends
- Judged by
- regex, select() options and grammar constraints enforced in code during generation
- Steers
- output that does not fit the constraint is blocked at decode time, and the program continues from the valid text
Install
pip install guidanceWhat it does not prove: It guarantees the output fits the declared pattern or choices, not that the chosen answer is correct. A model can still pick the wrong option from a valid list.
- LibraryMIT
Instructor
Gets typed, validated data out of an LLM using Pydantic models, and retries with the error message when validation fails.
- Proposes
- a structured answer (JSON) from a hosted or local LLM
- Judged by
- Pydantic validation of types and any custom validators you write
- Steers
- on a failed check, the validation error is sent back to the model and the call is retried
Install
pip install instructorWhat it does not prove: Passing validation shows the data fits the schema and your rules, not that it is true. Retries cost extra model calls and may still end in failure.
- ToolMIT
Kimina Lean Server
A server that checks Lean 4 code and proofs at scale, so a model's output gets a pass or fail from Lean.
- Proposes
- Lean 4 proofs and code from a model
- Judged by
- The Lean REPL running the code, served over an HTTP API
- Steers
- The check results go back to the caller, which can retry or filter the model's output
Install
pip install kimina-clientWhat it does not prove: A pass means Lean accepted the text it was given. It does not show the Lean statement says what the author meant. Running the server itself needs Lean and mathlib set up (the client pip package only talks to a server).
- ToolApache-2.0
Lean REPL
A JSON read-eval-print loop for Lean 4 that returns errors, unfinished-proof markers and proof states for any input.
- Proposes
- Lean commands and tactics from a person or model
- Judged by
- The Lean compiler and proof kernel
- Steers
- Error messages and remaining goals tell the caller what to try next
Install
lake exe replWhat it does not prove: It reports what Lean accepts, not whether the theorem is the one you wanted. A proof containing sorry is flagged but not rejected as a command. The README gives lake exe repl as the run command, after building the repo.
- LibraryMIT
LeanDojo
Python library that lets a program or model try proof steps in Lean and read back the new proof state or the error.
- Proposes
- Proof steps (tactics) from a prover model
- Judged by
- The Lean proof checker running the step
- Steers
- Lean's accepted or rejected result and the new goal guide the next step
Install
pip install lean-dojoWhat it does not prove: A proof Lean accepts is correct only for the theorem as stated in Lean. Whether the statement matches the intended claim is not checked. The README says this original library is deprecated in favor of LeanDojo-v2.
- ToolMIT
llama.cpp GBNF grammars
llama.cpp can restrict a local model's output to a formal grammar (GBNF), for example valid JSON or a chess move list.
- Proposes
- the next token from a local model run by llama.cpp
- Judged by
- the GBNF grammar, passed with --grammar-file or --grammar, checked in code at each step
- Steers
- only tokens that keep the text inside the grammar can be sampled
Install
curl -LsSf https://llama.app/install.sh | shWhat it does not prove: The grammar guarantees syntax only. A chess-format grammar will accept an illegal or silly move as long as it is written in the right notation.
llama.cpp repositoryllama.cpp README (install options)GBNF guideChecked
- LibraryBSD-2-Clause
LLM4AD
Platform for LLM-driven algorithm design: search methods like EoH and FunSearch, scored by task evaluators.
- Proposes
- LLM-written candidate algorithms
- Judged by
- task evaluation code (e.g. bin packing evaluators), run in separate processes with optional timeouts
- Steers
- search methods such as EoH and FunSearch pick which candidates are refined
Install
pip install llm4adWhat it does not prove: A good score shows an algorithm works on the benchmark instances used, not that it is the best possible or holds on other instances.
LLM4AD READMELLM4AD docsChecked
- LibraryApache-2.0
LMQL
A Python-based query language where you write where-constraints that the model's generated text must satisfy.
- Proposes
- text for each template variable in a query, from OpenAI or Hugging Face models
- Judged by
- the where clause, such as stops_at or type and content constraints, evaluated by the LMQL runtime
- Steers
- the runtime restricts what the model may generate so the constraints hold, and the program continues with the result
Install
pip install lmqlWhat it does not prove: Constraints check form and simple properties of the text, not whether the reasoning or facts are right. The README also shows a survey call for a next major version, so check how actively it is maintained.
LMQL repositoryLMQL READMEChecked
- LibraryApache-2.0
Math-Verify
Rule-based checker that parses an LLM's math answer and tests it against the gold answer, usable as a reward.
- Proposes
- nothing; it checks answers a model has already written
- Judged by
- parsing and symbolic comparison of the model answer against the gold answer, in code
- Steers
- its pass/fail result can serve as the reward when training a model, as the README recommends for reward verification
Install
pip install 'math-verify[antlr4_13_2]'What it does not prove: It checks that a final answer matches the reference, not that the reasoning is sound, and unusual answer formats can be missed or mismatched.
Math-Verify READMEChecked
- Code-run loopApache-2.0
OpenEvolve
Open-source AlphaEvolve-style loop: an LLM mutates programs and your scoring function picks which survive.
- Proposes
- LLM-written program mutations
- Judged by
- a user-supplied evaluator function that scores each program
- Steers
- MAP-Elites quality-diversity archive and island populations choose which programs get mutated next
Install
pip install openevolveWhat it does not prove: A high evaluator score shows a program does well on that scoring function, not that nothing better exists or that the evaluator captures what you really want.
OpenEvolve READMEPyPI pageChecked
- LibraryApache-2.0
Outlines
Forces a model's output to match a type, regex, choice list or grammar, so the structure is valid by construction.
- Proposes
- the next token of text from a local or hosted model
- Judged by
- a finite-state or grammar automaton built from the requested type, regex or grammar
- Steers
- tokens that would break the pattern are ruled out, so only valid continuations can be chosen
Install
pip install outlinesWhat it does not prove: It guarantees the shape of the output (valid JSON, a regex match, one of the listed choices), not that the values inside are true or sensible.
- LibraryApache-2.0
PyPantograph
Python interface to Lean 4 for running tactics step by step and checking a whole file matches its specification.
- Proposes
- Tactics and proof attempts from a prover model
- Judged by
- Lean, driven step by step, plus a whole-file conformity check (check_track)
- Steers
- Resulting goals and errors feed the search for the next tactic
Install
uv add git+https://github.com/stanford-centaur/PyPantographWhat it does not prove: A passing check shows the proof fits the stated Lean specification. It does not show the specification itself is the right one.
- Code-run loopApache-2.0
ShinkaEvolve
Sakana AI's program-evolution framework: an LLM edits code, an evaluation script scores it, an archive guides the search.
- Proposes
- LLM-written code edits
- Judged by
- an evaluation program you point it at (eval_program_path)
- Steers
- an archive of successful solutions shared across evolutionary islands decides what to evolve next
Install
pip install shinka-evolveWhat it does not prove: A better score means the program beats earlier candidates on your evaluation script, not that the result is optimal or generalizes beyond what that script tests.
ShinkaEvolve READMEChecked
- LibraryApache-2.0
XGrammar
Fast constrained-decoding engine that keeps LLM output inside a JSON schema, regex or context-free grammar.
- Proposes
- the next token from an inference engine such as vLLM or SGLang
- Judged by
- a compiled grammar matcher that checks which tokens keep the output grammatical
- Steers
- invalid tokens are masked out before sampling, so the output always follows the grammar
Install
pip install xgrammarWhat it does not prove: It guarantees structural correctness only, not that the content is accurate. A grammar that is too loose still lets nonsense through.