To support scalable oversight for AI systems capable of verified reasoning in interpreted formal languages, I developed the following packages which both provide methodology and tooling for advancing research in logic, semantics, and AI reasoning to support a safe digital future.
Model-Checker
The model-checkermodel-checker helps to prototype and combine semantic theories. These methods aim to support the growth and maturity of formal semantics as a discipline by easing the process of investigating increasingly complex theories for unified formal languages with an extensible collection of operators.
In addition to a general purpose methodology for rapidly prototyping modular semantic theories, the model-checker implements a semantics for the Logos which provides an extensible formal language of thought to equip AI agents with a capacity engage in verifiable reasoning in a formal language that is interpreted by explicit semantic models. More information about the methodology can be found in the GitHub repository.
I gave a talk at the Topos Institute presenting the broad outline of the project here.
Proof-Checker
The proof-checker implements the axiomatic proof system, recursive semantic theory, and metalogic for the Logos in LEAN. The Core Layer of the Logos implements a bimodal logic for tense and modality (TM) which combines an S5 modal logic for a historical modality with a linear tense logic for reasoning about past and future times in a history. The task semantics takes a non-deterministic dynamical system to provide the semantic foundation where possible worlds are functions from times to world states constrained by task relations, enabling reasoning about how different possibilities evolve through time.
The Core Layer includes eight axiom schemata and seven inference rules with proven soundness, along with perpetuity principles connecting modal and temporal operators. Beyond the Core Layer, the proof-checker implements a layered operator architecture for progressive extensibility. The Explanatory Layer will add counterfactual, causal, and constitutive operators; the Epistemic Layer will introduce belief, probability, and indicative operators; and the Normative Layer will provide deontic, agential, and preferential operators. Each layer shares task semantics and builds on the foundations established by the Core Layer, enabling increasingly sophisticated forms of verified reasoning.
Together with the model-checker, the proof-checker forms a dual verification architecture for training AI systems to reason in the Logos. The proof-checker generates positive RL signals by deriving valid theorems with machine-checkable proof receipts, while the model-checker generates corrective RL signals by producing explicit countermodels for invalid inferences. This architecture provides an unbounded source of clean training data: infinite theorems are derivable from the Logos axiom system, soundness guarantees that only valid inferences are rewarded, and LEAN proofs provide verifiable justifications while Z3 countermodels refute invalid claims. Unlike human reasoning data which is limited in quantify and complexity, inconsistent, and prone to error, training data generation with this dual verification architecture scales with computation rather than human annotation.