Constrained LLM generation via semantic invariants and refinement types.
invariants aims to guide large language model decoding by encoding semantic
constraints as refinement types and verifiable invariants.
The core runtime and DSL is written in C++ (lang/), with Python bindings
planned for integration into LLM inference pipelines.
Nix with flakes enabled is highly recommended. All compilers, build tools, and test dependencies are provided by the flake.
However, you are free to build and compile it yourself with CMake.
Read through the flake.nix to get an understanding of build-time requirements and whatnot.
nix developThis drops you into a shell with all relevant developer tooling available.
Run the configure step once (and again whenever CMakeLists.txt changes):
nix run .#configureThis generates .nix-dev/build/ with a compile_commands.json that both
clangd and the clang-tidy pre-commit hook read. This is also required for clangd,
if you use it.
We also provide a Nix app to run the test suite automatically:
nix run .#testThis also auto-generates the compilation database, but also runs ctest with the right arguments afterwards.
Note that both of these are impure, and are no better than simple Bash scripts! Be careful!
| Task | Command |
|---|---|
| Build & run all tests (Nix sandbox) | nix build |
Run the hello_world executable |
nix run |
CI runs nix build on every push and pull request targeting main.
prek is used for pre-commit automation.
Inside the dev shell, install the hooks once with:
prek installThe hooks run clang-format (Google style), clang-tidy, and cppcheck on
every commit. The clang-tidy hook requires the build directory to exist --
run nix run .#configure first if it doesn't (but this should be done automatically,
as it itself is the first hook run!).
lang/ C++ DSL runtime and syntax oracle (CMake project)
src/ Production source files
tests/ GoogleTest-based tests
bindings/ Python/C++ FFI (planned)
python/ Python package and LLM decoding loop (planned)
docs/ Notes and design drafts
See CONTRIBUTING.md for branching conventions, TDD guidelines, and merge strategy.