A Lean 4 system models patent claims as DAGs with match scores in a verified complete lattice and supplies kernel-checked certificates for coverage calculations and five IP use cases, conditional on unverified ML inputs.
Title resolution pending
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
years
2026 4roles
background 1polarities
background 1representative citing papers
A Datalog DSL is shallow-embedded in Lean with bidirectional interoperability and automatic translation of queries into provable theorems.
Alignment contracts define scope, allowed effects, budgets and disclosure rules as safety properties over finite effect traces, with decidable admissibility, refinement rules, and Lean-verified soundness under an observability assumption.
The paper argues that agent security is best addressed as a systems problem by applying principles from operating systems, networks, and formal methods rather than relying solely on model robustness improvements.
citing papers explorer
-
Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline
A Lean 4 system models patent claims as DAGs with match scores in a verified complete lattice and supplies kernel-checked certificates for coverage calculations and five IP use cases, conditional on unverified ML inputs.
-
A Shallow Embedding of Datalog in Lean
A Datalog DSL is shallow-embedded in Lean with bidirectional interoperability and automatic translation of queries into provable theorems.
-
Alignment Contracts for Agentic Security Systems
Alignment contracts define scope, allowed effects, budgets and disclosure rules as safety properties over finite effect traces, with decidable admissibility, refinement rules, and Lean-verified soundness under an observability assumption.
-
Agent Security is a Systems Problem
The paper argues that agent security is best addressed as a systems problem by applying principles from operating systems, networks, and formal methods rather than relying solely on model robustness improvements.