Skip to content
Change the repository type filter

All

    Repositories list

    • Cut vuln noise to near-zero by proving which CVEs are actually callable from your app’s entry points, using open CLIs, reproducible SBOMs, and CI-first workflows.
      Python
      0100Updated Sep 23, 2025Sep 23, 2025
    • Generate understanding, not just code. This toolkit helps teams reduce Time To Understanding (TTU) and Time To First Safe Change (TTFSC) with maps, traces, tours, contracts, and PR guardrails.
      HTML
      0100Updated Sep 23, 2025Sep 23, 2025
    • Provable AI agents with behavioral guarantees enforced by formal verification, runtime security, and end-to-end audit trails.
      Rust
      2934Updated Sep 16, 2025Sep 16, 2025
    • morph-replay-runner is a command-line interface (CLI) tool designed to execute TRACE-REPLAY-KIT bundles with branch-N parallelism on Morph Cloud. This tool streamlines the process of running replay tasks, ensuring efficient and scalable execution with comprehensive evidence collection and CERT-V1 compliance.
      Python
      0100Updated Aug 28, 2025Aug 28, 2025
    • Multiple SSE MCP servers behind a permissioning sidecar enforcing PERM-UNIFY-R1 (Call/Read/Write/Grant + epochs + IFC witnesses)
      Python
      0100Updated Aug 28, 2025Aug 28, 2025
    • A minimal, reusable CI template for running Lean 4 proofs on Morph Cloud's Infinibranch with intelligent caching and sharding.
      Python
      0100Updated Aug 28, 2025Aug 28, 2025
    • Automatically extracts hidden invariants from plain English specifications and generates formal proofs using Lean 4. Connect your Jira, Confluence, or Google Docs, and our NLP pipeline transforms natural language into mathematically verified guarantees.
      Rust
      0101Updated Aug 23, 2025Aug 23, 2025
    • SpecCursor is a GitHub App that autonomously upgrades dependencies, patches regressions using AI, and proves invariants using Lean 4.20. It provides a complete solution for maintaining software dependencies with confidence through formal verification.
      TypeScript
      0100Updated Aug 23, 2025Aug 23, 2025
    • A testbed for validating and demonstrating Provability Fabric's capabilities with observability, safety case management, external agent integration, and automated reporting.
      Python
      0100Updated Aug 23, 2025Aug 23, 2025
    • Machine-checks every fixed model artefact—weights, vocab, quant tables, tokenizers.
      Makefile
      0100Updated Aug 18, 2025Aug 18, 2025
    • Formal verification framework for dataset lineage, policy compliance, and training-time safety guarantees.
      Python
      0100Updated Aug 18, 2025Aug 18, 2025
    • State-of-the-art runtime safety components for AI model inference with formal proofs, ultra-low latency, and guaranteed correctness.
      Lean
      0100Updated Aug 18, 2025Aug 18, 2025
    • Transforms raw runtime telemetry into machine-checked forensic evidence—and proves that evidence can't be forged, lost, or silently falsified.
      Lean
      0100Updated Aug 18, 2025Aug 18, 2025
    • Formally verified deployment-boundary guarantees: RBAC, tenant isolation, SGX/SEV attestation, and compliance artifact generation with machine-checked proofs.
      Rust
      0100Updated Aug 18, 2025Aug 18, 2025
    • Lean Toolchain provides a collection of formally verified cryptographic algorithms, mathematical operations, and data parsing utilities. All implementations are proven correct in Lean 4 and can be extracted to high-performance Rust code.
      Lean
      0100Updated Aug 18, 2025Aug 18, 2025
    • Continuous Integration system that automatically diagnoses, patches, and validates code issues using AI-powered analysis and formal verification.
      TypeScript
      0100Updated Aug 11, 2025Aug 11, 2025
    • SpecSync

      Public
      Formal specification system that automatically analyzes code changes and generates comprehensive formal specifications using advanced LLM techniques and Lean4 theorem proving.
      JavaScript
      0100Updated Aug 4, 2025Aug 4, 2025