BOBCat

BOBCat is a goal-directed branch-coverage engine for Catala. It encodes branch objectives in Z3, decodes satisfying models into Catala inputs, and validates coverage by concrete replay. The implementation lives in compiler/bobcat/ and is exposed through the catala bobcat command.

BOBCat uses a fresh Z3 session for each branch goal and reuses that session through semantic refinement and timeout retries. Each query asks for the first satisfying model; the engine does not perform MaxSAT optimization.

This repository is based on the Catala compiler. The upstream Catala documentation follows.

Coverage comparison

The table below reports exact source-branch outcomes covered through only the public scopes declared in each <dataset>_wrapper.catala_* file. Adapter branches in the wrappers are excluded. Both engines ran with a 1,800-second limit per scope, 23 available workers, and maximum symbolic list length 5. The Aides logement row was rerun on 14 September 2026 after restoring archives.catala_fr; both engines include those historical rules and use the same 4,706-outcome denominator. This is one matched campaign, not a statistical estimate.

Coverage means the union of outcomes observed by replay-validated generated examples divided by all written branch outcomes in the definitions entered from those wrappers. CUTECat used its incremental/timeout configuration; BOBCat used progressive per-query Z3 limits from 2 to 60 seconds and ordinary SAT queries. Both received the same outer time and process parallelism budgets. The retained BOBCat dataset contains 402 validated tests.

The BOBCat figures are from the retained demand-driven campaign. They should not be read as an ablation of individual optimizations. Six wrappers timed out, and four ended with resource errors or SIGKILL after retaining their earlier validated tests. See the full configuration, comparison, and limitations.

BOBCat retains every model that completes concrete replay, including models whose observed path disagrees with their symbolic objective. Such a model is credited only for the branch outcomes actually observed; unresolved objectives are refined when supported. No coverage-based minimal-corpus pass is applied to BOBCat output.

---

Table of Contents

• Concepts
• The Catala book
• IDE Extensions and Tooling
  • Syntax highlighting
  • Catala VScode extension
  • Code formatting
• Documentation
  • Syntax cheat sheet
  • Formal semantics
  • Compiler documentation
• Examples
• API
• Contributing
• Test suite
• License
• Limitations and disclaimer
• Pierre Catala

Concepts

Catala is a programming language adapted for socio-fiscal legislative literate programming. By annotating each line of the legislative text with its meaning in terms of code, one can derive an implementation of complex socio-fiscal mechanisms that enjoys a high level of assurance regarding the code-law faithfulness.

Concretely, you have to first gather all the laws, executive orders, previous cases, etc. that contain information about the socio-fiscal mechanism that you want to implement. Then, you can proceed to annotate the text article by article, in your favorite text editor :

Once your code is complete and tested, you can use the Catala compiler to produce a lawyer-readable PDF version of your implementation. The Catala language has been specially designed in collaboration with law professionals to ensure that the code can be reviewed and certified correct by the domain experts, which are in this case lawyers and not programmers.

The Catala language is special because its logical structure mimics the logical structure of the law. Indeed, the core concept of "definition-under-conditions" that builds on default logic has been formalized by Professor Sarah Lawsky in her article A Logic for Statutes. The Catala language is the only programming language to our knowledge that embeds default logic as a first-class feature, which is why it is the only language perfectly adapted to literate legislative programming.

The Catala Book

The one-stop-shop for tutorials, installation instructions, FAQ and reference guide about Catala is the Catala book available at:

IDE Extensions and Tooling

Syntax highlighting

Syntax highlighting is available for several text-editors. Scripts can be found here.

Catala VSCode Extension

A VSCode extension for Catala is available on the marketplace. It bundles a syntax highlighter and a dedicated LSP server which offers support for code navigation, auto-completion along with a UX for test suites. See the dedicated repository for more details.

Code formatting

A code formatting tool, catala-format is available alongside the LSP server. If installed, code formatting is directly available in VSCode. This tool is based on a tree-sitter grammar for Catala. See the dedicated repository for more details.

Additional documentation items

Syntax cheat sheet

A complete and handy reference of the Catala syntax can be found in the cheat sheet (for French and English versions of the syntax).

Formal semantics

To audit the formal proof of the partial certification of the Catala compiler, see the dedicated readme.

Compiler documentation

The documentation is accessible online, for the latest master version.

It is otherwise generated from the compiler source code using dune and odoc. Run

make doc

to generate the documentation, then open the doc/odoc.html file in any browser.

Examples

To explore the different programs written in Catala, see the dedicated readme.

API

To know how to use the code generated by the Catala compiler in your favorite programming language, head to the readme of the French law library. The corresponding pre-built examples are also available.

Contributing

To know how you can contribute to the project, see the dedicated readme.

Test suite

To know how to run or improve the Catala reference test suite, see the dedicated readme.

License

The compiler and all the code contained in this repository is released under the Apache license (version 2) unless another license is explicited for a sub-directory.

Limitations and disclaimer

Catala is a research project from Inria, the French National Research Institute for Computer Science. The compiler is yet unstable and lacks some of its features.

Pierre Catala

The language is named after Pierre Catala, a professor of law who pioneered the French legaltech by creating a computer database of law cases, Juris-Data. The research group that he led in the late 1960s, the Centre d’études et de traitement de l’information juridique (CETIJ), has also influenced the creation by state conselor Lucien Mehl of the Centre de recherches et développement en informatique juridique (CENIJ), which eventually transformed into the entity managing the LegiFrance website, acting as the public service of legislative documentation.