Formal Methods Python Packages

pyvcg

Verification Condition Generator

miss-hit-core

MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more

miss-hit

MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more

percolation-inversion-compiler

AI agent output checker and workflow verification toolkit for turning agent text, pull requests, external inputs, and messages into auditable JSON reports with evidence routing, residual ledgers, provenance, and safe reuse checks.

maude

Language bindings for Maude

momba-engine

A toolbox for dealing with formal models from construction to analysis based on the JANI-model interchange format.

acacia-boomslang

Python bindings for Acacia-Bonsai, an antichain-based LTL synthesis and safety-game solver

cosa

CoreIR Symbolic Analyzer

recordflux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

vlabs-sdk

Public SDK and CLI for clean promotion gates, typed assurance cards, provider interfaces, and formal-spec mirrors.

agenticraft-foundation

Formally verified mathematical foundations for multi-agent AI coordination — CSP process algebra, multiparty session types, spectral topology, temporal logic model checking, and probabilistic verification.

momba

A toolbox for dealing with formal models from construction to analysis based on the JANI-model interchange format.

intrepyd

Intrepyd Model Checker

eventb-to-txt

Convert Event-B machines and contexts (.bum/.buc) to CamilleX plain-text models

racetrack

A toolbox for dealing with formal models from construction to analysis based on the JANI-model interchange format.

pythogic

Python package for deal with logical formulas and formal systems

punctilious

A human-friendly and developer-friendly math proof assistant

behaverify

BehaVerify: A Formal Verification Tool for Behavior Trees

re-technical-report

Technical report for the RE project.

panther-net

This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.

punt-z-spec

Z specification toolkit: type-checker, model-checker, and Claude Code plugin

astraintella

Verified AI reasoning SDK — formal verification layer between LLMs and constraint solvers

satisfaction-suffices

SAT-gated structural containment for AI — verification gate, four-verdict system, proof evolution, and paradox logic

tlacli

A wrapper script for running TLA+ from the command line