ProofForge

Quint

source-only .qnt · zero-tool finalize · deployable=false

目标

quint

族

可执行模型 / 规格

轨道

engineering

成熟度

source-only .qnt · zero-tool finalize · deployable=false

主制品

.qnt model source

工具锁定

产品 finalize 不调用 Quint CLI / Apalache（zero-tool）

可部署

false

Feature 清单

本目标的产品面计数（工程词汇，不是营销分数）。

7

合计

3

已支持

0

部分

3

显式拒绝

1

缺失

跨链对照：目标矩阵

执行模型

模型，非链

供模拟的状态机/关系面——无 settlement 轴。

Zero-tool finalize

成功与否与主机是否安装 Quint 无关。

pf.assets vault 模型

TipJar.qnt deposit/transfer 建模——非主网。

无 verify/ITF

quint verify / Apalache / ITF / MBT 不在 Q0 profile。

制品

文件角色
*.qnt主制品

Feature 列表

今天能 lower 什么、显式拒绝什么、仍缺失什么。

流水线

QuintPlan → 仅 .qnt 源。

1/3 已支持

  • SUPPORTED

    .qnt 物化

    Q0 materializer + inspect 闭包。

  • MISSING

    quint verify / Apalache

    仅未来 profile。

  • FAIL-CLOSED

    可部署制品

    本 profile 恒为 deployable=false。

Q0 面

窄单块 CFG；UInt64/Bool；pf.assets vault 子集。

2/4 已支持

  • SUPPORTED

    UInt64 / Bool 状态与算术

    完整 UInt64 域——禁止小域近似。

  • FAIL-CLOSED

    多块 CFG / 循环

    Q0 仅单块。

  • SUPPORTED

    pf.assets native vault 模型

    ADR-0029 Phase A

    TipJar demo 上 deposit/transfer 建模。

  • FAIL-CLOSED

    Option / Map / 聚合

    Q0 合法 Semantic 子集之外。

Profile

quint-source-u64-model-v1

Q0 单块 UInt64/Bool 模型；pf.assets vault 子集。

构建

lake env .lake/build/bin/proof-forge-next build \
  Examples/Counter.lean \
  --module Examples.Counter \
  --target quint -o build/counter-quint

lake env .lake/build/bin/proof-forge-next inspect build/counter-quint --json
开放名单 →目标矩阵 →