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

acacia-boomslang

A minimal implementation of reactive synthesis via universal co-Buchi automata using antichains

maude

Language bindings for Maude

verifier-standard

VSTD: portable, bounded, refutable evidence for computational claims and provenance graphs.

intrepyd

Intrepyd Model Checker

plan-auditor

Make an AI agent's 'done' mean 'here is the command output that proves it.' Deterministic, LLM-free verification for AI coding agents: sealed plans, SHA-256 hash-chained evidence, STRIPS/PDDL reachability, and a fail-closed completion gate.

momba-engine

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

recordflux

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

cosa

CoreIR Symbolic Analyzer

punt-z-spec

Creates, validates, and animates Z (and B) specifications from source and generates code from specifications

sentil

Runtime verification for Probabilistic Signal Temporal Logic

momba

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

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.

reasonsmith

Prove which legally-owed reasons a decision system deleted, and from whom — by re-running its own inference, not reading its log. Every verdict states how it was reached.

hypermath-foundations

A closed formal universe derived from one primitive operation, with a Lean translation and a reproducible audit that publishes its own open obligations.

racetrack

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

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.

re-technical-report

Technical report for the RE project.

pythogic

A Python package for deal with logical formulas and formal systems (e.g. FOL)

eventb-to-txt

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

metaspace-membrane

A deterministic, deny-by-default safety membrane for machine-generated software. One .bio constitution, three membranes, two products. Patent pending.

holosim

Deterministic continuity and verification framework for preserving corrections, uncertainty, evidence, and reconstruction across AI and software handoffs.