CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

Proof of thought : LLM-based reasoning using Z3 theorem proving with multiple backend support (SMT2 and JSON DSL)

A Machine-to-Machine Interaction System for Lean 4.

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

LatPlan : A domain-independent, image-based classical planner

Automatic programming by creating Pull Requests from Issues using LLMs

Logic Circuits from the Juice library

configurable, high-performance SAT solver, implementing incremental solving interface of MiniSat and IPASIR. Based on MiniSat (minisat.se)

AI Agents for Academic Writing. Ingests PDFs or markdown → outputs publish-ready LaTeX with verified citations and TikZ diagrams. One click.

An automated deductive program verifier based on concurrent separation logic

MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers

Automated reasoning based on the Laws of Intelligence naturally embedded in the human language • Open source software • Multilingual, including Chinese

A lightweight Description Logic reasoner for large-scale biomedical ontologies

Representation learning for ontologies and their annotations

Distributed constraint satisfaction with recursive message-passing agents

Bayesian Ontology Reasoner

Reasoner for the description logic EL+.

A novel approach to learning concept embeddings and approximate reasoning in ALC knowledge bases with neural networks

Imandra Modelling Language CME MDP Model