Leibniz Labs

Leibniz Labs is associated with Erik Meijer’s research into verifying AI-agent actions before execution. Meijer proposes having agents generate an inspectable computation rather than act directly, then checking that computation against formalized requirements. The approach addresses practical concerns such as unauthorized spending and information leakage.

Meijer’s Universalis research describes a programming language within a proposed AI-first program-synthesis framework, designed for knowledge workers to read and for accompanying tools to analyze and manipulate. Meijer also connects Automind and Universalis to his published research on using large language models as neural computers.

His proposed verification architecture uses Horn clause logic and SMT solvers to check generated plans against business rules. A user’s request becomes a specification; the model generates a program, and an independent verifier checks it before execution. This makes the specification an explicit part of the workflow: developers must formalize the rules against which an agent’s proposed behavior will be judged.