c-parser，autocorres都是在Isabelle上形式验证c代码的工具，它们都是seL4项目的一部分，而这些所有的工具都是主要基于Linux的，所以建议在Linux上安装，以下内容是在WSL上安装的过程。
进行安装前必要的步骤：
- 支持WSL图形化的Windows系统，我个人用的是win10专业版，没有这个就别往下看了，别的系统我都没测试过
- 开启WSL图形化，具体工作可以参考微软官方文档，我的经验是，只要能打开Nautilus就说明WSL GUI是正常的。
安装Isabelle
根据官网要求，下载安装包，解压后，就可以使用Isabelle了。个人使用的是Isabelle2023，建议使用相同的版本。
首先测试一下Isabelle2023能否正常运行，直接在命令行里运行Isabelle2023（应用程序就叫这个名字）
./Isabelle2023/Isabelle2023
如果能够正常显示Isabelle的JEditor，说明安装正确。
确定安装正确后，将Isabelle命令行工具加入环境变量方便使用，命令行工具所在的路径为Isabelle2023/bin/
加入环境变量后可以测试一下，如果能够直接从命令行调用isabelle命令，那么就说明成功了。
安装证明环境
首先从github上clone seL4有关证明的项目到本地
git clone https://github.com/seL4/l4v.git
我们来看一下项目的目录格式，这里只列出我们需要关心的文件夹
l4v-+
|-isabelle 这是一个软连接，请调整这个软链接使它指向你自己的Isabelle文件夹根目录
|-tools--+
|-c-parser
|-autocorres
里面已经包含了autocorres和c-parser
安装c-parser
安装c-parser之前需要先安装MLton，这个直接参照MLton官网下载链接的安装要求应该就可以。
首先来到c-parser文件夹下面，我们按照文件夹中的INSTALL文件的指令运行如下命令
export L4V_ARCH=X64 #我第一次用ARM似乎也成功了，不知道为啥，明明我电脑是X64的，总之你们多试试
isabelle env make CParser
如果没有产生错误，那么c-parser的安装就完成了
安装autocorres
在l4v文件夹下面运行命令
L4V_ARCH=X64 misc/regression/run_tests.py AutoCorres
如果没有产生问题，那么就安装完成了
运行项目
想要在Isabelle上使用我们刚才安装的两个工具，请按照如下命令运行你的项目
isabelle jedit -d 你的l4v项目根文件夹路径 -l CParser 你要打开的thy文件
可以使用这个thy文件作为例子，测试一下环境是否征程
theory scratch
imports "CParser.CTranslation" AutoCorres.AutoCorres
begin
install_C_file minmax.c
autocorres minmax.c
context minmax begin
thm min_body_def
thm min'_def
thm max_body_def
lemma min'_is_min: "min' a b = min a b"
unfolding min_def min'_def
by (rule refl)
end
end
注意，theory后面的名字应该根据你的文件名修改，使其保持一致。