PrincetonUniversity/DeepSpecDB 开源项目中文解读：技术栈、适用场景与上手建议

GNU Lesser General Public License v3.0

项目介绍

PrincetonUniversity/DeepSpecDB 是一个托管在 GitHub 上的开源项目，主要使用 Rocq Prover 编写，采用 GNU Lesser General Public License v3.0 许可证，目前获得 28 个 Star、3 次 Fork。

仓库全名: PrincetonUniversity/DeepSpecDB
开源许可证: GNU Lesser General Public License v3.0
Star 数: 28
Fork 数: 3
未关闭 Issue: 1

README 摘要

This is the DeepSpecDB project at Princeton University. This work is distributed under the terms of the LGPL v3 license. See the COPYING and COPYING.LESSER file for information. It includes (slightly modified) work from the FormalData/SqlEngines project, available at https://framagit.org/formaldata [May 2019]. This project is experimental. It includes work on the verification of: B+trees, B+tree cursors (as in…

完整内容见 GitHub 原始 README 或本页。

常见问题

DeepSpecDB 用什么语言开发？

主要使用 Rocq Prover 编写，采用 GNU Lesser General Public License v3.0 许可证，目前有 28 个 Star。

DeepSpecDB 可以免费商用吗？

仓库标注的许可证为 GNU Lesser General Public License v3.0，商用前请先阅读仓库 LICENSE 文件确认授权范围。

如何获取 DeepSpecDB 的源码？

可以直接克隆仓库：git clone https://github.com/PrincetonUniversity/DeepSpecDB.git，默认分支为 master；安装与运行步骤见仓库 README。

DeepSpecDB 最近还在维护吗？

仓库最近一次更新为 2025年11月21日，当前有 1 个未关闭 Issue；Star 数为 28，可作为社区活跃度的参考。

简要分析

热度分

价值分

活跃状态

活跃

暂无主题

GitHub

语言占比

BibTeX Style

Makefile

OCaml

Rocq Prover

Shell

TeX

贡献者

README

This is the DeepSpecDB project at Princeton University.

This work is distributed under the terms of the LGPL v3 license. See the COPYING and COPYING.LESSER file for information. It includes (slightly modified) work from the FormalData/SqlEngines project, available at https://framagit.org/formaldata [May 2019].

This project is experimental. It includes work on the verification of: B+trees, B+tree cursors (as in SQLite), Tries of keyslices of B+trees (as in Masstree), Malloc/free systems, database low-level algorithms: sequential scan, index scan, index join.

The folder structure is as follows:

/src contains C code for cursored B+trees, Masstree-like key-value store, as well as some low-level RDBMS algorithms. This is the work of Oluwatosin Adewale (B+trees and Masstree from 2018) and Pablo Le Hénaff (database algorithms from 2019).
/model contains Coq code for a B+tree model by Brian McSwiggen
/tuplekey contains a C implementation written by Prof. Andrew Appel of concatenated, composite-key indices. It has both object-oriented and first-order code.
/verif contains Coq code for the Verifiable C verification of the C code contained in /src. – /verif/btrees contains Oluwatosin Adewale’s B+trees verification by Aurèle Barrière (March - June 2018) – /verif/tries contains Oluwatosin Adewale’s masstree-like key-value store verification by Luke Xuan. – /verif/db contains (highly experimental) verification attempts of Pablo Le Hénaff’s low-level algorithms code This folder also contains a modified copy of the work of DataCert from https://framagit.org/formaldata [May 2019]. This code has been studied (Pablo) for interfacing the low-level algorithms functional model with the top part of the verified SQL query compilation pipeline from DataCert. This is explained in details in the /paper/Pablo folder. – /verif/indices contains some verification of the concatenated indices in /tuplekey

The folders in /verif usually contain a copy of the C code at stake, slightly modified for the purpose of Verifiable C verification.

/memmgr contains attemps at verification of malloc and free (see the included README)

DeepSpecDB