hyperpolymath/proven
GitHub: hyperpolymath/proven
基于 Idris 2 依赖类型的形式化验证安全库，通过数学证明保证数学运算、加密、解析和验证操作永不崩溃，支持 120+ 语言绑定。
Stars: 2 | Forks: 0
= proven: 通过 Idris2 实现形式化验证的安全
:toc: macro
:toclevels: 2
:icons: font
:source-highlighter: rouge
*数学上证明安全的操作。* **绝不会崩溃**的代码，通过 Idris2 依赖类型和全函数检查进行验证。
image:https://img.shields.io/badge/version-1.2.0-blue[版本 1.2.0]
image:https://img.shields.io/badge/License-PMPL_1.0--or--later-blue.svg[PMPL-1.0-or-later,link="https://github.com/hyperpolymath/proven/blob/main/LICENSE"]
image:https://img.shields.io/badge/modules-104-blue[104 个模块]
image:https://img.shields.io/badge/bindings-120+_targets-orange[120+ 绑定目标]
image:https://img.shields.io/badge/verified-Idris_2-purple[通过 Idris 2 验证]
image:https://img.shields.io/badge/believe__me-4566_⚠-red[believe_me = 4566 (已知技术债务)]
image:https://img.shields.io/badge/overall-55%25-yellow[总体完成度 55%]
== 许可证
本项目采用 **PMPL-1.0-or-later** 许可。详见 link:LICENSE[LICENSE]。
WARNING: **proven** 是一个 **带有 FFI 绑定的 Idris2 库**，而不是你使用的语言的原生实现。所有计算都在 Idris2 中进行，并具有数学证明。语言绑定通过 FFI 调用此经过验证的代码。
IMPORTANT: **坚不可摧的保证仅适用于 Idris2 代码。** Zig 层必须是*纯 ABI 桥接*，不包含任何安全逻辑。绑定中任何非 Idris 逻辑均被视为未经验证，必须移除。
== proven 有何不同？
*传统库：* 相信作者做对了 +
*proven：* **数学证明**代码不会崩溃
=== 架构
```
Your Application (any of 120+ languages)
↓
Language Binding (thin FFI wrapper)
↓
Zig FFI Bridge (pure ABI layer)
↓
Idris2 Code ← MATHEMATICAL PROOFS HERE
```
**核心实现：** link:src/Proven/[带依赖类型的 Idris2] +
**FFI 桥接：** link:ffi/zig/[用于 C ABI 兼容性的 Zig]（无安全逻辑） +
**语言绑定：** 仅调用已验证代码的轻量级封装
== 性能权衡
纯 Idris ABI 最大化了安全性，但引入了 FFI 开销。这是一个
深思熟虑的权衡：**正确性优于速度**。性能改进将
专注于批处理和减少交叉调用，而不会重新引入未经证明的逻辑。
== 迁移状态
该项目正将所有绑定迁移至**纯 Zig ABI 封装**，仅调用
Idris。绑定中任何非 Idris 安全逻辑正被移除或重写。
=== 支持的语言
[.lead]
*通用：* Ada • C • C++ • Crystal • D • Dart • Deno • Elixir • Elm • Erlang • F# • Gleam • Go • Groovy • Haskell • Java • JavaScript • Julia • Kotlin • Lua • Nim • OCaml • Odin • Perl • PHP • Prolog • PureScript • Python • R • Racket • ReScript • Ruby • Rust • Scala • Swift • Tcl • TypeScript • V • Zig
*Shell:* Bash • Fish • PowerShell • Zsh | *函数式:* Clojure • Common Lisp • Guile | *遗留:* COBOL • Forth • Fortran
*配置:* CUE • Dhall • HCL • Jsonnet • JSON-Schema • Nickel • Starlark • YAML-Schema
*领域:* Arduino • Cairo • CMake • GDScript • Ink • MicroPython • Move • Solidity • Svelte • Unity C# • Vue • Vyper
*查询/策略:* CEL • GraphQL • PromQL • Rego | *形式化:* Alloy • TLA+ | *操作系统:* BSD • POSIX
*异构计算:* Janus (可逆) • 神经形态 (SNN) • OpenQASM (量子) • Q# (量子) • SPICE (模拟) • 三进制 (平衡)
*底层:* AssemblyScript • Grain • Malbolge • VHDL • WAT | *伪代码:* Pseudocode
== 模块索引
[cols="1,3", options="header"]
|===
| 类别 | 模块
| *核心安全*
| <> • <> • <> • <> • <> • <>
| *数据格式*
| <> • <> • <> • <> • <> • <> • <> • <> • <> • <> • <> • <>
| *Web 与网络*
| <> • <> • <> • <> • <> • <> • <> • <> • <>
| *安全与认证*
| <> • <> • <> • <> • <> • <> • <> • <> • <>
| *容器与镜像仓库*
| <>
| *输入验证*
| <> • <> • <> • <> • <>
| *系统与 I/O*
| <> • <> • <> • <> • <> • <> • <> • <> • <> • <> • <> • <> • <>
| *高级/分布式*
| <> • <> • <> • <> • <> • <>
| *专用*
| <> • <> • <> • <>
| *数学与物理*
| <> • <> • <> • <> • <> • <> • <>
| *分布式系统*
| <> • <> • <> • <>
| *数据结构*
| <> • <> • <> • <> • <> • <> • <> • <> • <>
| *领域值*
| <> • <> • <> • <>
| *DevOps 与工具*
| <> • <> • <>
| *国际化*
| <>
|===
=== 绑定统计
[cols="1,1,1", options="header"]
|===
| 指标 | 数量 | 备注
| 核心模块
| 104
| Idris 2 验证过的实现（共 258 个 .idr 文件，包括 FFI 封装）
| 绑定目标
| 120+
| 语言、平台和范式（18 个已完成，102 个已搭建脚手架）
| believe_me 计数
| 0
| 已从约 4,566 个实例中消除（于 2026-02-22 修复）
| 总体完成度
| ~55%
| 核心稳固 (100%)，应用 (7%)，硬件 (0%)，便利层 (0%)
|===
=== 绑定类别
[cols="1,1,2", options="header"]
|===
| 类别 | 数量 | 描述
| 通用
| 39
| 传统编程语言 (C, Rust, Python, Go 等)
| Shell/脚本
| 4
| Bash, Fish, PowerShell, Zsh
| 配置
| 8
| CUE, Dhall, HCL, Jsonnet, Nickel, Starlark, JSON/YAML Schema
| 领域特定
| 12
| 游戏开发、区块链、嵌入式、Web 框架
| 查询/策略
| 4
| CEL, GraphQL, PromQL, Rego
| 异构计算
| 6
| 量子 (OpenQASM, Q#), 模拟 (SPICE), 神经形态, 三进制, 可逆 (Janus)
| 形式化方法
| 2
| TLA+, Alloy - 规范语言
| 特定操作系统
| 2
| POSIX 系统调用, BSD (Capsicum, pledge/unveil)
| 底层
| 5
| WebAssembly, VHDL, AssemblyScript, Grain, Malbolge
| 遗留
| 3
| COBOL, Fortran, Forth
| 函数式/Lisp
| 3
| Clojure, Common Lisp, Guile
| 伪代码
| 1
| 人类可读的算法文档
|===
toc::[]
== 问题所在
## [source,python]
# 你凌晨 3 点的代码
## result = 10 / user_input # ZeroDivisionError
data = json.loads(response)["key"] # KeyError
url = urllib.parse.urlparse(user_url) # Malformed URL? Who knows
password = hashlib.md5(pwd).hexdigest() # You just got hacked
regex = re.compile(user_input) # ReDoS attack waiting to happen
html = "" # XSS vulnerability
command = "rm -rf " + user_input # Shell injection
sql = "SELECT * FROM users WHERE name = '" + user_input + "'" # SQL injection
每一行都可能导致你的应用崩溃或制造安全漏洞。
== 解决方案
## [source,python]
from proven import SafeMath, SafeJson, SafeUrl, SafePassword, SafeRegex, SafeHtml, SafeCommand, SafeSql
# 绝不能崩溃。永不。数学上已证明。
## result = SafeMath.div(10, user_input) # 如果为零返回 None，而非异常
data = SafeJson.get(response, "key") # Returns None if missing, typed if present
url = SafeUrl.parse(user_url) # Returns structured error or valid URL
hashed = SafePassword.hash(pwd) # Argon2id, timing-safe, correct parameters
matcher = SafeRegex.compile(user_input, safety=SafeRegex.Safety.STRICT) # ReDoS-proof
safe_html = SafeHtml.escape(user_html) # XSS-proof
command = SafeCommand.build(["rm", "-rf", user_path]) # Injection-proof
query = SafeSql.query("SELECT * FROM users WHERE name = ?", [user_input]) # SQL injection-proof
== “数学上证明”意味着什么
这不是营销噱头。以下是 proven 与普通库的区别：
* proven 中的每个函数都是用 Idris 2 编写的，这是一种具有依赖类型的语言。
* 编译器在代码运行之前就证明了你的代码是正确的。
* 所有 104 个核心模块都有经过验证的实现（自 v1.2.0 起 believe_me=0）。存在 120+ 个绑定目标（18 个完全实现，102 个搭建了 FFI 桩）。总体项目完成度约 55% — 详见 link:TOPOLOGY.md[TOPOLOGY.md] 仪表盘。
=== 理解依赖类型（2 分钟入门）
在大多数语言中，类型与值是分离的：
## [source,python]
## def get_first(items: list) -> int:
return items[0] # Crashes if empty!
类型系统不知道列表是否为空。它只是信任你。
在 Idris 2 中，类型可以依赖于值：
## [source,idris]
## -- 此类型签名要求一个非空列表
getFirst : (items : List Int) -> {auto prf : NonEmpty items} -> Int
`{auto prf : NonEmpty items}` 部分的意思是：“调用者必须提供 items 非空的证明。”如果你尝试用空列表调用它，代码将无法编译。
这是核心理念：用编译时错误代替运行时崩溃。
=== 这如何转化为你的代码
[cols="1,1"]
|===
| 普通代码 | Proven 代码
| “我认为这不会崩溃”
| “编译器证明了这不可能崩溃”
| “我测试过，没问题”
| “在编译时检查了所有可能的输入”
| “它通过了代码审查”
| “定理证明器验证了它”
|===
=== 想了解更多？
证明可在 `src/Proven/` 中找到，我们鼓励你探索它们！理解依赖类型是一项宝贵的技能。这里有一些资源：
* https://idris2.readthedocs.io/en/latest/[Idris 2 教程] — 依赖类型的官方介绍
* https://www.youtube.com/watch?v=__gXFtYmDnQ[Type-Driven Development with Idris] — Edwin Brady 的演讲
* link:docs/PROOFS.md[我们的文档] — 解释本库中的每个证明
也就是说，你完全可以在不理解证明的情况下使用该库——形式化验证的意义就在于编译器已经为你检查了正确性。
== 模块
=== SafeMath — 不会溢出的算术
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `div(a, b)`
| 安全除法，除零时返回 `None`
| `ZeroDivisionError`
| `add_checked(a, b)`
| 带溢出检测的加法
| 静默整数溢出
| `mul_checked(a, b)`
| 带溢出检测的乘法
| 整数溢出利用
| `safeMod(a, b)`
| 安全取模，除零时返回 `None`
| 除以零
| `abs_safe(n)`
| 绝对值（处理 MIN_INT）
| abs(MIN_INT) 时的溢出
| `clamp(lo, hi, value)`
| 将值限制在 [lo, hi] 范围内
| 越界值
| `inRange(value, lo, hi)`
| 检查值是否在边界内
| 差一错误
| `inRangeExcluding(value, lo, hi, excluded)`
| 带排除列表的范围检查
| 禁止值绕过
| `fromString(str)`
| 安全整数解析
| `NumberFormatException`, NaN
| `fromStringInRange(str, lo, hi)`
| 带范围验证的解析
| 无效输入 + 越界
|===
## [source,python]
from proven import SafeMath
## SafeMath.div(10, 2) # 5
SafeMath.div(10, 0) # None (not an exception!)
SafeMath.add_checked(2**63 - 1, 1) # None (overflow detected)
SafeMath.add_checked(5, 3) # 8
=== SafeString — 不会损坏的文本
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `decode_utf8(bytes)`
| 安全 UTF-8 解码
| `UnicodeDecodeError`
| `escape_sql(s)`
| SQL 注入预防
| SQL 注入攻击
| `escape_html(s)`
| XSS 预防
| 跨站脚本攻击
| `escape_js(s)`
| JavaScript 字符串转义
| 字符串中的 JS 注入
| `truncate(s, n)`
| 安全截断（尊重字素）
| 在表情符号中间截断
| `toCodePoints(s)`
| 将字符串转换为 ASCII 码位
| 编码损坏
| `fromCodePoints(codes)`
| 将码位转换为字符串
| 无效字符创建
| `isAscii(s)`
| 检查字符串是否为纯 ASCII (0-127)
| 非 ASCII 字节注入
| `isPrintableAscii(s)`
| 检查字符串是否为可打印 ASCII (32-126)
| 控制字符注入
|===
## [source,python]
from proven import SafeString
## SafeString.decode_utf8(b"\xff\xfe") # None (无效 UTF-8)
SafeString.decode_utf8(b"hello") # "hello"
SafeString.escape_sql("'; DROP TABLE users;--") # "'' ; DROP TABLE users;--" (neutralized)
=== SafeHex — 不会损坏的十六进制
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `encode(bytes)`
| 将字节转换为十六进制字符串
| 编码错误
| `encodeUppercase(bytes)`
| 将字节转换为大写十六进制
| 大小写不一致
| `encodeSpaced(bytes)`
| 带空格的十六进制显示 (`48 65 6c`)
| 可读性问题
| `encodeSpacedUppercase(bytes)`
| 大写带空格的十六进制
| 显示格式错误
| `decode(hex)`
| 将十六进制字符串转换为字节
| 无效十六进制时的 `ValueError`
| `isValidHex(s)`
| 验证十六进制字符串格式
| 畸形十六进制绕过
| `constantTimeEqual(a, b)`
| 时序安全的十六进制比较
| 时序攻击
| `xorHex(a, b)`
| 对两个十六进制字符串进行异或
| 长度不匹配错误
|===
## [source,python]
from proven import SafeHex
## SafeHex.encode([72, 101, 108, 108, 111]) # "48656c6c6f"
SafeHex.encodeSpaced([72, 101, 108]) # "48 65 6c"
SafeHex.decode("48656c6c6f") # [72, 101, 108, 108, 111]
SafeHex.decode("invalid") # Error(InvalidCharacter)
SafeHex.constantTimeEqual("abc", "abc") # True (timing-safe)
=== SafeJson — 不会意外失败的解析
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `parse(s)`
| 安全 JSON 解析
| `JSONDecodeError`
| `get(obj, key)`
| 安全键访问
| `KeyError`
| `get_path(obj, path)`
| 安全嵌套访问
| 链式 `KeyError`
| `get_int(obj, key)`
| 类型化提取
| 类型混淆
|===
## [source,python]
from proven import SafeJson
## data = SafeJson.parse('{"name": "Alice", "age": 30}')
SafeJson.get(data, "name") # "Alice"
SafeJson.get(data, "missing") # None
SafeJson.get_int(data, "age") # 30
SafeJson.get_int(data, "name") # None (wrong type)
SafeJson.parse("not json") # Error object with details, not exception
=== SafeUrl — 无法被利用的 URL
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `parse(s)`
| 符合 RFC 3986 的解析
| 畸形 URL 崩溃
| `is_safe_redirect(url, allowed)`
| 开放重定向预防
| 开放重定向攻击
| `normalize(url)`
| URL 规范化
| URL 绕过攻击
| `get_path_safe(url)`
| 无遍历的路径
| `../../../etc/passwd`
|===
## [source,python]
from proven import SafeUrl
url = SafeUrl.parse("https://example.com/path?query=1#hash")
url.scheme # "https"
url.host # "example.com"
url.path # "/path"
## SafeUrl.parse("not a url") # 错误对象，而非异常
SafeUrl.is_safe_redirect("https://evil.com", allowed=["example.com"]) # False
=== SafeHTTP — URL 编码与认证头解析
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `url_encode(s)`
| RFC 3986 百分号编码
| URL 注入、畸形参数
| `url_decode(s)`
| 带验证的百分号解码
| 双重编码攻击
| `parse_www_authenticate(header)`
| OAuth2/Registry 质询解析
| 认证头注入
|===
## [source,python]
from proven import SafeHTTP
encoded = SafeHTTP.url_encode("hello world") # "hello%20world"
decoded = SafeHTTP.url_decode("hello%20world") # "hello world"
# 解析 Docker Registry v2 认证质询
## challenge = SafeHTTP.parse_www_authenticate(
'Bearer realm="https://auth.io/token",service="registry"'
)
challenge.realm # "https://auth.io/token"
challenge.service # "registry"
=== SafeRegistry — OCI 镜像引用解析
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `parse(ref)`
| 解析 [registry/]repo[:tag][@digest]
| 畸形镜像引用
| `normalize(ref)`
| 应用 Docker Hub 默认值
| 镜像仓库混淆攻击
| `has_digest(ref)`
| 检查内容寻址引用
| 可变标签漏洞
|===
## [source,python]
from proven import SafeRegistry
ref = SafeRegistry.parse("ghcr.io/user/repo:v1.0")
ref.registry # "ghcr.io"
ref.repository # "user/repo"
ref.tag # "v1.0"
# Docker Hub 简写
ref = SafeRegistry.parse("nginx")
ref.registry # "docker.io" (default)
ref.repository # "library/nginx" (official images)
ref.tag # "latest" (default)
# 摘要固定引用
## ref = SafeRegistry.parse("nginx@sha256:abc123...")
ref.has_digest # True
ref.to_canonical() # "docker.io/library/nginx:latest@sha256:abc123..."
=== SafeDigest — 加密哈希操作
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `parse(digest)`
| 解析 "algorithm:hex" 格式
| 畸形摘要、长度错误
| `verify(expected, actual)`
| 常量时间比较
| 摘要验证中的时序攻击
| `is_valid(digest)`
| 验证摘要字符串
| 无效哈希格式
|===
## [source,python]
from proven import SafeDigest
digest = SafeDigest.parse("sha256:e3b0c44298fc1c149afbf4c8...")
digest.algorithm # SHA256
digest.value # "e3b0c44298fc1c149afbf4c8..."
# 常量时间验证（抵抗计时攻击）
expected = SafeDigest.parse("sha256:abc123...")
actual = SafeDigest.parse("sha256:abc123...")
SafeDigest.verify(expected, actual) # True (constant-time)
# 支持 SHA256, SHA384, SHA512, Blake3
## SafeDigest.is_valid("sha512:cf83e1357eefb8bd...") # True
SafeDigest.is_valid("md5:abc123") # False (insecure algorithm)
=== SafeEmail — 真正有效的验证
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `is_valid(s)`
| 符合 RFC 5321 的检查
| 接受无效电子邮件的错误正则
| `parse(s)`
| 提取本地/域部分
| 通过电子邮件字段注入
| `normalize(s)`
| 小写、修剪、规范化
| 大小写敏感错误
|===
## [source,python]
from proven import SafeEmail
SafeEmail.is_valid("user@example.com") # True
SafeEmail.is_valid("not an email") # False
SafeEmail.is_valid("user@localhost") # True (valid per RFC)
## email = SafeEmail.parse("User@Example.COM")
email.local # "user"
email.domain # "example.com" (normalised)
=== SafePath — 无法逃逸的文件系统访问
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `join_safe(base, user_path)`
| 安全路径连接
| 路径遍历攻击
| `is_within(path, base)`
| 检查包含关系
| 目录逃逸
| `sanitize(filename)`
| 移除危险字符
| 空字节注入、特殊字符
|===
## [source,python]
from proven import SafePath
## SafePath.join_safe("/var/uploads", "file.txt") # "/var/uploads/file.txt"
SafePath.join_safe("/var/uploads", "../../../etc/passwd") # Error: path traversal detected
SafePath.sanitize("file\x00.txt") # "file.txt" (null byte removed)
=== SafeCrypto — 你不会搞砸的密码学
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `hash_sha3(data)`
| SHA-3 哈希
| 使用破碎的算法
| `hash_blake3(data)`
| BLAKE3 哈希
| 哈希速度慢
| `random_bytes(n)`
| 加密随机性
| 在安全场景使用 `random.random()`
| `constant_time_eq(a, b)`
| 时序安全比较
| 时序攻击
|===
## [source,python]
from proven import SafeCrypto
## token = SafeCrypto.random_bytes(32) # 加密随机性
digest = SafeCrypto.hash_sha3(b"data")
digest = SafeCrypto.hash_blake3(b"data") # Faster
SafeCrypto.constant_time_eq(user_token, stored_token) # Timing-safe
=== SafePassword — 正确完成的认证
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `hash(password)`
|on2id 哈希
| MD5, SHA1, bcrypt 弱点
| `verify(password, hash)`
| 时序安全验证
| 时序攻击
| `is_strong(password)`
| 强度检查
| 弱密码
|===
## [source,python]
from proven import SafePassword
hashed = SafePassword.hash("user_password") # Argon2id
if SafePassword.verify("user_password", hashed):
print("Login successful")
## SafePassword.is_strong("password123") # False
SafePassword.is_strong("c0rr3ct-h0rs3-b4tt3ry-st4pl3") # True
=== SafeRegex — 不会 ReDoS 的正则表达式
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `compile(pattern, safety)`
| 复杂度受限的正则
| 灾难性回溯
| `test(pattern, input)`
| 安全正则匹配
| ReDoS 攻击
| `match(pattern, input)`
| 安全正则捕获
| 资源耗尽
|===
## [source,python]
from proven import SafeRegex
## matcher = SafeRegex.compile("((a+)+)", safety=SafeRegex.Safety.STRICT) # 拒绝危险模式
SafeRegex.test("^[a-z]+$", "abc123") # False (safe matching)
=== SafeHTML — 无法 XSS 的 HTML
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `escape(content)`
| 上下文感知转义
| XSS 攻击
| `sanitize(html, policy)`
| 基于白名单的清理
| 脚本标签注入
| `element(tag, attrs, children)`
| 类型安全的 HTML 构建
| 畸形 HTML
|===
## [source,python]
from proven import SafeHtml
## safe = SafeHtml.escape("") # "<script>..."
sanitized = SafeHtml.sanitize("hello", policy=SafeHtml.Policy.STANDARD)
div = SafeHtml.element("div", {"class": "safe"}, ["Hello"])
=== SafeCommand — 无法注入的 Shell 命令
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `build(args)`
| 安全命令构建
| Shell 注入
| `escape(arg)`
| 参数转义
| 元字符利用
| `is_dangerous(command)`
| 危险模式检测
| 意外的危险命令
|===
## [source,python]
from proven import SafeCommand
## command = SafeCommand.build(["grep", user_input, "file.txt"]) # 防注入
SafeCommand.escape("; rm -rf /") # Escaped string
=== SafeSQL — 无法注入的 SQL
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `query(sql, params)`
| 参数化查询
| SQL 注入
| `identifier(name)`
| 安全标识符引用
| 表/列注入
| `is_safe(sql)`
| 注入分析
| 意外漏洞
|===
## [source,python]
from proven import SafeSql
## query = SafeSql.query("SELECT * FROM users WHERE name = ?", [user_input])
SafeSql.identifier("user_table") # Safely quoted identifier
=== SafeJWT — 无法伪造的 Token
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `sign(payload, key, algorithm)`
| 安全 JWT 签名
| 算法混淆
| `verify(token, key)`
| 时序安全验证
| Token 篡改
| `decode(token)`
| 安全载荷提取
| 畸形 Token
|===
## [source,python]
from proven import SafeJwt
## token = SafeJwt.sign({"user": 123}, "secret", algorithm="HS256")
payload = SafeJwt.verify(token, "secret")
=== SafeNetwork — 无法被滥用的网络原语
[cols="1,1,1"]
|===
| 函数 | 功能 | 防止的问题
| `parse_ip(s)`
| IPv4/IPv6 解析
| 无效 IP 崩溃
| `parse_cidr(s)`
| CIDR 表示法解析
| 子网计算错误
| `is_valid_port(n)`
| 端口验证
| 无效端口号
|===
## [source,python]
from proven import SafeNetwork
## ip = SafeNetwork.parse_ip("192.168.1.1")
cidr = SafeNetwork.parse_cidr("192.168.1.0/24")
SafeNetwork.is_valid_port(8080) # True
== 高级模块
这些模块为分布式系统、状态机和资源管理提供形式化验证的实现。
=== SafeStateMachine — 带可逆性证明的状态机
类型安全的状态机，无效转换为编译时错误。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `ReversibleOp`
| 带正向/反向函数的操作
| `inverse . forward = id`
| `HistoryMachine`
| 带撤销/重做的状态机
| 撤销返回到先前状态
| `DFA`
| 确定性有限自动机
| 确定性地接受/拒绝
| `GuardedTransition`
| 带前置/后置条件的转换
| 条件得到满足
|===
=== SafeGraph — 带环检测证明的有向图
类型安全的有向图和 DAG，带有编译时无环证明。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `DAG`
| 有向无环图类型
| 图不包含环
| `Acyclic`
| 无环证明
| 拓扑排序存在
| `topoSort`
| 拓扑排序
| 输出遵循边顺序
| `PathExists`
| 路径存在证明
| 可达性已验证
|===
=== SafeTransaction — 带隔离证明的 ACID 事务
形式化验证的事务语义，带有提交/回滚保证。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `IsolationLevel`
| 读未提交到可串行化
| 隔离保证成立
| `Transaction`
| 类型化事务状态
| Active/Committed/RolledBack 状态
| `TwoPhaseCommit`
| 分布式提交协议
| 全有或全无语义
| `MVCC`
| 多版本并发
| 快照隔离正确性
|===
=== SafeConsensus — 带法定人数证明的分布式共识
Raft 和 Paxos 共识原语，带有数学法定人数保证。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Quorum`
| 多数证明类型
| `votes > total / 2`
| `RaftNode`
| Raft 协议状态机
| 领导者选举正确性
| `VectorClock`
| 因果关系跟踪
| 发生于之前关系
| `Agreement`
| 共识协定证明
| 所有已决定节点具有相同值
|===
=== SafeCapability — 带委托证明的基于能力的安全
类型安全的能力，带有权限层次结构和撤销。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Capability`
| 权限授予类型
| 持有者拥有权限
| `attenuate`
| 减少权限
| 新权限 ⊆ 原始权限
| `ConfinedCapability`
| 域受限能力
| 无法泄漏到域外
| `AuditedStore`
| 带审计日志的能力存储
| 所有访问均被记录
|===
=== SafeOrdering — 带因果关系证明的时序排序
发生于之前关系和带有传递性证明的逻辑时钟。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `HappensBefore`
| Lamport 排序关系
| 传递性成立
| `VectorTimestamp`
| 向量时钟实现
| 正确捕获因果关系
| `CausalDelivery`
| 因果消息排序
| 消息按顺序传递
| `PlausibleClock`
| 混合逻辑时钟
| 物理/逻辑一致性
|===
=== SafeResource — 带泄漏预防的资源生命周期
线性资源跟踪，带有 RAII 风格保证。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Resource`
| 类型化生命周期状态
| 状态转换有效
| `Linear`
| 一次性语义
| 资源恰好使用一次
| `ResourcePool`
| 有界资源池
| 池永不过载
| `LeakDetector`
| 跟踪获取/释放
| 当 `NoLeaks` 成立时无泄漏
|===
=== SafeSchema — 带兼容性证明的 Schema 迁移
类型安全的 Schema 演进，带有向前/向后兼容性保证。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Migration`
| 带 up/down 的 Schema 更改
| 回滚逆转迁移
| `isBackwardCompatible`
| 兼容性检查
| 旧读取器可读新数据
| `MigrationChain`
| 迁移序列
| 链是连续的
| `VersionedSchema`
| 带弃用的 Schema
| 弃用时间线已跟踪
|===
=== SafeFloat — IEEE 754 浮点安全
溢出、下溢和浮点特殊值处理。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `FiniteFloat`
| 非 NaN、非 Inf 浮点数
| 值是有限的
| `safeDiv`
| 带 NaN/Inf 检查的除法
| 结果有效或为错误
| `safeSqrt`
| 非负数的平方根
| 输入非负
| `ULP`
| 最后一位单位
| 精度界限
|===
=== SafeTensor — 维度安全的张量操作
形状检查的张量操作，用于数值计算。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Tensor`
| N 维数组
| 形状静态已知
| `matmul`
| 矩阵乘法
| 内部维度匹配
| `broadcast`
| 形状广播
| 满足广播规则
| `reshape`
| 张量重塑
| 元素数量保持不变
|===
=== SafeML — 机器学习安全
类型安全的 ML 原语，带有数值稳定性保证。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Probability`
| [0,1] 中的值
| 满足边界
| `softmax`
| 数值稳定的 softmax
| 输出总和为 1
| `crossEntropy`
| 安全交叉熵损失
| 无 log(0) 错误
| `normalize`
| 安全归一化
| 处理零向量
|===
=== SafePolicy — AST 级策略执行
基于区域的策略执行，带有冲突检测和审计跟踪。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `ZoneClass`
| 可变/不可变/混合/受限区域
| 区域边界受尊重
| `PolicyRule`
| 条件操作规则
| 规则确定性地评估
| `evaluatePolicy`
| 上下文策略评估
| 第一个匹配规则生效
| `findConflicts`
| 检测规则冲突
| 无同优先级矛盾
|===
=== SafeBuffer — 有界缓冲区管理
具有溢出预防证明的固定容量缓冲区。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Buffer`
| 固定容量缓冲区
| 计数 ≤ 容量
| `HasSpace`
| 空间可用性证明
| 写入将成功
| `RingBuffer`
| 循环缓冲区
| 环回正确
| `StreamBuffer`
| 感知背压的缓冲区
| 尊重高/低水位线
|===
=== SafeProvenance — 带审计证明的变更跟踪
数据血缘和审计跟踪完整性验证。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `ProvenanceChain`
| 哈希链接的变更历史
| 链完整性可验证
| `Lineage`
| 数据派生跟踪
| 来源归属保留
| `AuditTrail`
| 密封审计日志
| 密封后无修改
| `detectTampering`
| 篡改检测
| 哈希链完整
|===
=== SafeTree — 带覆盖证明的树遍历
类型安全的树构建、和操作。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `DepthTree`
| 深度跟踪树类型
| 不能超过最大深度
| `ValidPath`
| 到节点的路径证明
| 导航将成功
| `TreeZipper`
| 高效导航
| 往返保留结构
| `mapTree`
| 转换所有值
| 结构保留
|===
== 数学与物理模块
=== SafeAngle — 带回绕安全的角度处理
类型安全的角度操作，带有自动规范化和单位转换。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Angle`
| 弧度角 (-π, π]
| 值始终规范化
| `fromDegrees`
| 从度数转换
| 正确转换
| `sin`, `cos`, `tan`
| 三角函数
| 处理边缘情况
| `lerp`, `slerp`
| 角度插值
| 采用最短路径
|===
=== SafeProbability — 带分布操作的概率值
类型安全的概率值，保证在 [0, 1] 范围内，带有贝叶斯操作。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Probability`
| [0, 1] 中的值
| 满足边界
| `bayesUpdate`
| 后验计算
| 结果在有效范围内
| `shannonEntropy`
| 信息熵
| 处理边缘情况
| `Distribution`
| 概率分布
| 值总和为 1
|===
=== SafeUnit — 带量纲分析的物理单位
类型安全的物理量，带有编译时量纲检查。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Quantity`
| 带量纲的值
| 单位被跟踪
| `mul`, `div`
| 量算术
| 量纲正确计算
| `convert`
| 单位转换
| 相同量纲
| `add`
| 量相加
| 需要相同量纲
|===
=== SafeFiniteField — 有限域算术
用于密码学的素域 GF(p) 和二元域 GF(2^n) 算术。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `PrimeField`
| GF(p) 算术
| 运算 mod p
| `BinaryField`
| GF(2^n) 算术
| 多项式算术
| `inverse`
| 模逆
| 扩展欧几里得算法
| `legendre`
| 二次剩余测试
| 正确计算符号
|===
== 分布式系统模块
=== SafeMonotonic — 单调计数器和逻辑时钟
用于分布式系统的 Lamport 时钟、混合逻辑时钟和版本向量。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `MonotonicCounter`
| 永不递减计数器
| 单调性保持
| `LamportClock`
| 逻辑时间戳
| 捕获因果关系
| `HybridLogicalClock`
| 物理 + 逻辑时间
| 有界时钟偏差
| `VersionVector`
| 分布式因果关系
| 发生于之前关系
|===
=== SafeRateLimiter — 带令牌桶和滑动窗口的速率限制
类型安全的速率限制，带有可配置策略。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `TokenBucket`
| 令牌桶算法
| 速率有界
| `LeakyBucket`
| 流量整形
| 输出速率受限
| `SlidingWindow`
| 基于窗口的计数
| 计数准确
| `AdaptiveRateLimiter`
| 动态调整
| 响应负载
|===
=== SafeCircuitBreaker — 容错熔断器模式
熔断器模式的状态机实现。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `CircuitBreaker`
| 闭合/断开/半开状态
| 有效状态转换
| `recordSuccess`
| 跟踪成功调用
| 状态正确更新
| `recordFailure`
| 跟踪失败
| 阈值检查
| `allowRequest`
| 检查是否允许请求
| 依赖状态的决定
|===
=== SafeRetry — 带指数退避的重试策略
可配置的重试机制，带有抖动和截止时间。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `RetryConfig`
| 重试策略配置
| 有效参数
| `exponentialBackoff`
| 指数延迟增长
| 受最大延迟限制
| `jitter`
| 随机化延迟
| 防止惊群效应
| `DeadlineRetryState`
| 感知截止时间的重试
| 尊重截止时间
|===
== 数据结构模块
=== SafeQueue — 有界队列和优先队列
类型安全的带背压支持的有界队列。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `BoundedQueue`
| 固定容量队列
| 大小 ≤ 容量
| `PriorityQueue`
| 最小堆优先队列
| 顺序保持
| `RingBuffer`
| 循环缓冲区
| 环回正确
| `BackpressureQueue`
| 高/低水位线
| 信号受尊重
|===
=== SafeBloom — 带误报率界限的布隆过滤器
空间高效的概率数据结构，带有 FPR 保证。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `BloomFilter`
| 固定大小过滤器
| FPR 可计算
| `optimalBits`
| 计算最优大小
| 针对目标 FPR 最小化
| `CountingBloomFilter`
| 支持移除
| 计数有界
| `ScalableBloomFilter`
| 按需增长
| FPR 保持
|===
=== SafeLRU — 带 TTL 支持的 LRU 缓存
带生存时间和统计信息的有界 LRU 缓存。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `LRUCache`
| 最近最少使用驱逐
| 大小 ≤ 容量
| `TimedLRUCache`
| 带 TTL 的条目
| 尊重过期
| `StatsLRUCache`
| 命中/未命中跟踪
| 准确统计
| `hitRate`
| 计算命中率
| 正确计算
|===
== 领域值模块
=== SafeColor — 带色域钳制的颜色处理
类型安全的颜色，带有转换和 WCAG 可访问性合规。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `RGB`, `RGBA`
| [0, 255] 中的颜色值
| 边界强制
| `rgbToHsl`, `hslToRgb`
| 颜色空间转换
| 正确变换
| `contrastRatio`
| WCAG 对比度计算
| 可访问性检查
| `parseHex`
| 十六进制颜色解析
| 有效格式
|===
=== SafeGeo — 带距离计算的地理坐标
类型安全的纬度/经度，带有半正矢距离和方位角计算。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `Latitude`
| [-90, 90] 中的值
| 有效范围
| `Longitude`
| [-180, 180] 中的值
| 已规范化
| `haversineDistance`
| 大圆距离
| 正确计算
| `BoundingBox`
| 地理边界
| 有效矩形
|===
=== SafeVersion — 语义版本解析和比较
符合 SemVer 2.0.0 的版本解析，带有范围约束。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `SemVer`
| Major.minor.patch
| 有效组件
| `parseSemVer`
| 解析版本字符串
| 符合 SemVer
| `compareSemVer`
| 版本比较
| 正确排序
| `VersionRange`
| 约束检查
| 可满足性检查
|===
=== SafeChecksum — CRC 和哈希函数
用于数据完整性的非加密校验和和哈希。
[cols="1,1,1"]
|===
| 特性 | 功能 | 证明内容
| `crc32`, `crc32c`
| CRC-32 变体
| 正确多项式
| `adler32`
| Adler-32 校验和
| 正确算法
| `fletcher16/32/64`
| Fletcher 校验和
| 正确计算
| `luhnValidate`
| Luhn 算法
| 数字验证
|===
== 安装
=== Rust
## [source,bash]
## cargo add proven
=== Deno / JavaScript
## [source,bash]
# Deno (推荐)
import { SafeMath, SafeJson } from "jsr:@proven/core";
# Node.js
## npx jsr add @proven/core
=== Python
## [source,bash]
# 使用 pipx (推荐)
pipx install proven
# 使用 pip
## pip install proven
=== Go
## [source,bash]
## go get github.com/hyperpolymath/proven
=== Zig
## [source,bash]
# 添加到您的 build.zig
## executable.addModule("proven", .{
.source_file = .{ .file = "path/to/proven.zig" }
})
=== Guile Scheme
## [source,bash]
# 添加到加载路径
export GUILE_LOAD_PATH="/path/to/proven/bindings/guile:$GUILE_LOAD_PATH"
# 在 Guile 中
## (use-modules (proven))
=== Nickel
## [source,nickel]
# 导入库
## let proven = import "path/to/proven.ncl" in
{
server.port | proven.SafeNetwork.Port = 8080,
}
=== 开发环境（Idris 2 核心）
## [source,bash]
# 主要 (pack)
pack install-deps
# Guix 回退
guix time-machine -C guix/channels.scm -- \
shell -m guix/manifest.scm
# Nix 回退
nix-shell nix/shard.nix
# 锁定周期 (Guix master + nixpkgs-unstable)
# 每月第一个周六，加上 CVE 驱动的更新：
## ./scripts/update-env-pins.sh
=== 89 个绑定目标
适用于传统语言、配置语言、领域特定语言和异构计算范式的绑定。有关特定语言的文档，请参阅 `bindings/` 目录。
除传统语言外的重要新增内容：
* **量子计算**：OpenQASM 3.0, Q# - 安全量子位操作、有界角度、概率验证
* **模拟计算**：SPICE - 有界电压/电流源、用于电路模拟的安全运算放大器
* **神经形态**：尖峰神经网络 - 安全膜电位、STDP、LIF 神经元
* **可逆计算**：Janus - 带朗道极限跟踪的双射操作
* **三进制计算**：平衡三进制（Setun 兼容）- 安全 tryte 算术
* **形式化方法**：TLA+, Alloy - 安全不变量的规范
* **操作系统安全**：POSIX 系统调用封装，BSD Capsicum/pledge/unveil
== 工作原理（好奇者进阶）
## [ascii]
## ┌─────────────────────────────────────────────────────────────────┐
│ Your App (120+ targets) │
│ Traditional languages • Config • Domain-specific • Exotic │
└─────────────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────────┐
│ Language Bindings (auto-generated) │
│ Python: ctypes | Rust: bindgen | JS: WebAssembly │
│ Go: cgo | Zig: native | Quantum: OpenQASM/Q# | SPICE: lib │
└─────────────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────────┐
│ Zig FFI Bridge Layer │
│ Cross-platform • Memory safe • Stable ABI guaranteed │
│ (see: github.com/hyperpolymath/idris2-zig-ffi) │
└─────────────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────────┐
│ Idris 2 Verified Core (v1.1.0) │
│ │
│ • 104 modules with dependent types: compiler PROVES code ││ is correct │
│ • Total functions: every input produces valid output │
│ • No runtime exceptions: impossible by construction │
│ • ECHIDNA integration for CI verification │
│ │
│ Used by: aerospace, automotive, financial, blockchain │
│ Inspiration: HACL* (Firefox, Linux kernel, WireGuard) │
└─────────────────────────────────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────────┐
│ Verification Layer │
│ ECHIDNA (multi-prover) ◄─── echidnabot (CI) │
│ Coq │ Lean │ Agda │ Z3 │ Idris2 │
└─────────────────────────────────────────────────────────────────┘
== 常见问题
Q: 这会很慢吗？::
不。Idris 2 编译成 C，然后由 Zig 优化。基准测试显示大多数操作的性能在手写 C 的 5-15% 以内。加密函数通常更快，因为它们使用避免分支预测错误的常量时间实现。
Q: 我需要学习 Idris 2 吗？::
完全不需要（但你会爱上它的！）。该库绑定的工作方式类似于你语言中的任何标准库。但是，如果你对形式化验证感兴趣，理解 Idris 2 源代码将帮助你理解为什么保证如此强大。
Q: 如果我发现错误怎么办？::
如果你在 proven 中发现错误，你可能发现了以下之一的错误：
1. 语言绑定（我们的错误，请报告）
2. Idris 2 编译器（极其罕见）
3. 你对函数的理解（查看文档）
核心逻辑在数学上是经过证明的。但绑定是由人类编写的。
Q: 为什么不直接使用现有的库？::
[cols="1,1"]
|===
| 库 | 问题
| `json` (Python)
| 对无效输入抛出异常
| `hashlib` (Python)
| 允许你使用 MD5、SHA1 和其他破碎的算法
| `urllib` (Python)
| API 复杂，容易误用，可能发生路径遍历
| `bcrypt` (多种)
| 静默地将密码截断为 72 字节
| `random` (Python)
| 非加密安全（人们仍然用它生成令牌）
|===
Q: 这是否可用于生产环境？::
是的，自 v1.0.0 起。所有核心模块和绑定均已完成。安全审计已通过，全面的测试套件，以及用于证明验证的 ECHIDNA 集成。
Q: 我正在使用 Rust... 我的代码难道不是无敌的吗？
Rust 的借用检查器和内存安全保证非常出色，但它们并不涵盖所有崩溃向量：
* 逻辑错误（例如，整数溢出、不正确的业务逻辑）仍然可能通过。
* 如果不进行审计，FFI/unsafe 块可能会引入漏洞。
* 并发错误（例如，死锁、竞态条件）无法在编译时捕获。
* 生态系统风险（例如，依赖项中的 unsafe、不正确的 panic 处理）仍然存在。
proven 通过以下方式补充 Rust：
* 为逻辑添加形式化验证（例如，SafeMath, SafeRegex）。
* 为常见陷阱提供防崩溃抽象（例如，SafePath, SafeSql）。
* 为 Rust 提供 Zig FFI 绑定，以利用 proven 的验证模块，而无需重写代码库。
* ECHIDNA 集成用于关键路径的 CI 验证。
把它想象成你无敌跑车的安全带。
Q: 我正在使用 Python... 我以为代码就是注定要崩溃的？
Python 的动态性很强大，但崩溃并非不可避免！proven 的 Python 绑定让你能够：
用编译时保证（通过 Idris 2 证明）替换 try/except 意大利面代码。
为容易出错的操作使用类型安全的替代方案：
* SafeJson.parse() → 不再有 KeyError 或 JSONDecodeError。
* SafePath.join_safe() → 不再有 ../../../etc/passwd 利用。
* SafeRegex.compile() → 不再有 ReDoS 攻击。
在消除整类运行时错误的同时保持 Python 的人体工程学。
性能开销？~1–5%（几乎总是比手写的防御性代码快）。
崩溃是一种选择。选择不崩溃。
== 路线图
=== v1.1.0（当前版本）
* ✅ 104 个核心模块，带有依赖类型证明（从 v1.0.0 的 74 个扩展）
* ✅ Zig 桥接层的 14 个新 FFI 导出
* ✅ SPDX 头标准化为 PMPL-1.0-or-later
* ✅ 证明修复：SafeCapability, ECHIDNA/Soundness, SafeFloat
* ✅ SafeCert FFI 主机名匹配与源模块对齐
* ✅ SafeML FFI parsePositive 替换为标量构建块
* ✅ ipkg 重复模块条目已清理
* ✅ 所有 TODO 桩转换为文档注释
=== v1.0.0
* ✅ 初始版本，包含 74 个核心模块和依赖类型证明
* 120+ 绑定目标通过 Zig FFI（18 个完成，102 个搭建脚手架）
* ✅ 带模糊测试的完整测试套件
* ✅ 安全审计通过
* ✅ CI/CD 基础设施
* ✅ ECHIDNA 集成用于证明验证
=== 下一步（2026 年第二季度）
* ❏ 镜像仓库发布（crates.io, PyPI, npm, JSR）
* ❏ 后量子密码（Dilithium, Kyber）
* ❏ WebAssembly 浏览器包
* ❏ IDE 插件（VS Code, IntelliJ）
=== 未来
* ❏ 形式化方法研讨会和教程
* ❏ 更多语言绑定（Zig 原生, Mojo）
* ❏ 硬件安全模块（HSM）支持
* ❏ FIPS 140-3 认证路径
== 贡献
我们欢迎贡献！详见 link:CONTRIBUTING.adoc[CONTRIBUTING.adoc]。
特别需要：
* 语言绑定维护者（Scala, F#, Crystal 等）
* 安全审查员
* 文档撰写者
* 测试用例贡献者
* ECHIDNA 证明器后端开发者
== 相关项目
[cols="1,2"]
|===
| 项目 | 简介
| https://github.com/hyperpolymath/echidna[echidna]
| 神经符号定理证明平台。proven 的 Idris 2 证明可由 ECHIDNA 的多证明器系统验证。
| https://github.com/hyperpolymath/echidnabot[echidnabot]
| ECHIDNA 的 CI 编排。修改 proven 的 PR 通过 echidnabot Webhooks 触发自动证明验证。
| https://github.com/hyperpolymath/aggregate-library[aggregate-library]
| 跨 7 种语言的通用操作。proven 提供 aLib 操作的形式化验证 Idris 2 实现。
| https://github.com/hyperpolymath/idris2-zig-ffi[idris2-zig-ffi]
| 使该库可从 44 种语言调用的 FFI 桥接。
| https://github.com/hyperpolymath/januskey[januskey]
| 使用 SafeCrypto, SafePassword 和 SafeStateMachine 进行可逆操作的密钥管理系统。
| https://github.com/hyperpolymath/git-hud[git-hud]
| 使用 SafeConsensus 进行分布式操作和 SafeGraph 进行依赖跟踪的 Git 仓库管理器。
| https://github.com/hyperpolymath/ubicity[ubicity]
| 使用 SafeSchema 进行迁移和 SafeOrdering 进行事件溯源的数据平台。
| https://github.com/stefan-hoeck/idris2-pack[idris2-pack]
| Idris 2 的包管理器 - proven 通过 pack 分发。
|===
== 许可证
本项目采用 PMPL-1.0-or-later 许可。详见 link:LICENSE[LICENSE]。
== 安全
有关报告漏洞，请参阅 link:SECURITY.md[SECURITY.md]。
*别再奢望代码不崩溃。确信它不会崩溃。*
_引用本工作：_ 详见 link:docs/PAPER.tex[arXiv 论文] 以获取学术引用。
标签：AI工具, API密钥检测, CMS安全, FFI, Go, Idris2, JavaScript, JSONLines, Python, Ruby工具, Rust, TLS抓取, WebAssembly, YAML, Zig, 不可变, 云安全监控, 代码生成, 依赖类型, 函数式编程, 可视化界面, 多语言绑定, 安全库, 安全计算, 密码学, 形式化验证, 手动系统调用, 数学证明, 数据可视化, 无后门, 无崩溃, 日志审计, 渗透测试工具, 类型安全, 系统编程, 网络流量审计, 解析器, 跨语言调用, 软件安全, 输入验证, 边缘计算安全, 逆向工具, 防御性编程, 零信任, 静态分析, 高可靠性