Enterprise-grade formal verification framework for machine learning models with support for large-scale transformers, vision models, and distributed verification.
- Overview
- Key Features
- Architecture
- Quick Start
- Installation
- Usage
- Documentation
- Contributing
- License
FormalVerifML is a state-of-the-art framework for formally verifying machine learning models using Lean 4. It provides comprehensive support for verifying properties such as robustness, fairness, interpretability, and safety across a wide range of model architectures.
To provide mathematically rigorous verification of ML models for high-stakes applications in healthcare, finance, autonomous systems, and other critical domains where model reliability is paramount.
- Mathematical Rigor: Uses Lean 4 theorem prover for formal mathematical proofs
- Production Ready: Enterprise features with multi-user support, audit logging, and security
- Scalable: Supports models up to 100M+ parameters with distributed verification
- Comprehensive: Vision transformers, large-scale models, and advanced architectures
- Automated: SMT solver integration for automated proof generation
- Neural Networks: Feed-forward, convolutional, recurrent architectures
- Transformers: Full transformer support with multi-head attention
- Vision Models: ViT, Swin Transformers, CLIP-style multi-modal models
- Large-Scale Models: 100M+ parameter models with distributed processing
- Decision Trees: Interpretable tree-based models
- Linear Models: Logistic regression and linear classifiers
- Robustness: Adversarial robustness and input perturbation resistance
- Fairness: Demographic parity, equalized odds, individual fairness
- Interpretability: Attention analysis, feature attribution verification
- Safety: Causal masking, sequence invariance, memory efficiency
- Performance: Memory optimization, distributed verification
- Multi-User Support: Role-based access control and session management
- Audit Logging: Comprehensive activity tracking and compliance
- Security: Rate limiting, encryption, and input validation
- Distributed Processing: Multi-node verification with fault tolerance
- Monitoring: Real-time performance metrics and health checks
FormalVerifML/
├── lean/ # Lean 4 formal verification code
│ ├── FormalVerifML/
│ │ ├── base/ # Core definitions and properties
│ │ ├── generated/ # Auto-generated model definitions
│ │ └── proofs/ # Verification proof scripts
├── translator/ # Model translation and testing
│ ├── export_from_pytorch.py # PyTorch model export
│ ├── generate_lean_model.py # JSON to Lean code generation
│ └── test_*.py # Comprehensive test suites
├── webapp/ # Web interface and visualization
├── docs/ # Documentation and guides
└── .github/ # CI/CD and workflows
- Model Export: PyTorch/HuggingFace models → JSON format
- Code Generation: JSON → Lean 4 definitions
- Verification: Lean 4 → Formal proofs of properties
- Results: Web interface visualization and reports
- Docker (recommended) or Python 3.9+ and Lean 4
- 8GB+ RAM for large model verification
- Modern web browser for the interface
# Clone the repository
git clone https://github.com/fraware/formal_verif_ml.git
cd formal_verif_ml
# Build and run with Docker
docker build -t formalverifml .
docker run -p 5000:5000 -v $(pwd)/models:/app/models formalverifml
# Access the web interface
open http://localhost:5000# Clone the repository
git clone https://github.com/fraware/formal_verif_ml.git
cd formal_verif_ml
# Install Python dependencies
pip install -r translator/requirements.txt
# Install Lean 4 (see https://leanprover.github.io/lean4/doc/setup.html)
# Then build the project
lake build
# Run the web interface
python webapp/app.py# Export a PyTorch model
python translator/export_from_pytorch.py \
--model_path your_model.pth \
--output_path model.json \
--model_type transformer# Convert JSON to Lean definitions
python translator/generate_lean_model.py \
--model_json model.json \
--output_lean lean/FormalVerifML/generated/my_model.lean# Build and verify with Lean
lake build
lake exe FormalVerifMLUpload your model JSON files through the web interface at http://localhost:5000 to:
- Visualize model architecture
- Generate Lean code automatically
- Run verification proofs
- View detailed logs and results
- User Guide: Getting started and basic usage
- Developer Guide: Architecture and extension guide
- Lean API: Core definitions and properties
- Python API: Model translation and testing tools
- Web API: Web interface and visualization
# Comprehensive test suite
python translator/run_comprehensive_tests.py
# Enterprise feature tests
python translator/test_enterprise_features.py
# HuggingFace model tests
python translator/test_huggingface_models.py- ✅ Model Loading: PyTorch and HuggingFace model compatibility
- ✅ Code Generation: JSON to Lean translation accuracy
- ✅ Verification: Property verification correctness
- ✅ Performance: Memory usage and execution time
- ✅ Enterprise: Multi-user, security, and audit features
We welcome contributions! Please see our Contributing Guidelines for details.
# Clone and setup development environment
git clone https://github.com/fraware/formal_verif_ml.git
cd formal_verif_ml
# Install development dependencies
pip install -r translator/requirements.txt
pip install -r requirements-dev.txt
# Setup pre-commit hooks
pre-commit install
# Run tests
python -m pytest tests/- Python: Follow PEP 8 with type hints
- Lean: Use Lean 4 style guide and mathlib conventions
- Documentation: Comprehensive docstrings and comments
- Testing: 90%+ test coverage required
This project is licensed under the MIT License - see the LICENSE file for details.
- Lean Community: For the excellent theorem prover
- HuggingFace: For transformer model support
- PyTorch Team: For the deep learning framework
- Contributors: All who have helped improve this project
- Issues: GitHub Issues
- Discussions: GitHub Discussions
- Documentation: Project Wiki
Made with ❤️ by the FormalVerifML Team