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
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
years
2026 6roles
background 1polarities
background 1representative citing papers
Kani is a model checker that compiles Rust proof harnesses from MIR to CBMC for bounded verification of safety properties and supports contracts to extend checks to unbounded correctness.
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.
KYA provides a framework-agnostic trust layer using inbound pipelines, policy composition, unified trust scoring, interaction multipliers, and delegation attribution to ensure authorized, conforming, and verifiable actions in autonomous systems.
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.
-
Kani: A Model Checker for Rust
Kani is a model checker that compiles Rust proof harnesses from MIR to CBMC for bounded verification of safety properties and supports contracts to extend checks to unbounded correctness.
-
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.
-
KYA: A Framework-Agnostic Trust Layer for Autonomous Systems with Verifiable Provenance and Hierarchical Policy Composition
KYA provides a framework-agnostic trust layer using inbound pipelines, policy composition, unified trust scoring, interaction multipliers, and delegation attribution to ensure authorized, conforming, and verifiable actions in autonomous systems.
-
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.