typetheoryforall/FVjobs

选用指南

AI 根据 README 整理 · 2026/10/27 10:11:27

使用方式

通过网页浏览职位表格，数据由data/jobs.yml生成，可通过提交issue或修改YAML文件并运行脚本添加职位。

查看 README 依据

| **Last verified** | When a human last confirmed the posting was live | Some entries also record work authorization, published pay, and a short note. Those live in [`data/jobs.yml`](data/jobs.yml), which is the source of truth — the table above is generated from it. Closed roles move to [`data/archive.yml`](data/archive.yml) rather than being deleted: knowing that a company was hiring for Lean work six months ago is useful even when the posting is gone. ## Adding a job Open a [new job issue](../../issues/new?template=new-job.yml) — it is a short

form, and no Git required. If you would rather send a pull request, add an entry to `data/jobs.yml` and run: ```bash pip install pyyaml jsonschema python3 scripts/validate.py python3 scripts/render.py ``` See [CONTRIBUTING.md](CONTRIBUTING.md) for what belongs here and what does not. ## Scope In scope: roles whose core work is formal verification or closely supports it — proof engineering, automated reasoning, verified compilation, hardware formal verification, program analysis built on formal semantics, and AI-for-proof work.

部署要求

添加职位需安装Python依赖pyyaml和jsonschema，并运行验证与渲染脚本。

查看 README 依据

form, and no Git required. If you would rather send a pull request, add an entry to `data/jobs.yml` and run: ```bash pip install pyyaml jsonschema python3 scripts/validate.py python3 scripts/render.py ``` See [CONTRIBUTING.md](CONTRIBUTING.md) for what belongs here and what does not. ## Scope In scope: roles whose core work is formal verification or closely supports it — proof engineering, automated reasoning, verified compilation, hardware formal verification, program analysis built on formal semantics, and AI-for-proof work.

已知限制

明确排除无验证内容的通用编译器、系统岗位及纯应用安全岗位。

查看 README 依据

Out of scope: general compiler and systems roles with no verification content, "security engineer" roles that are really appsec, and anything where the connection to formal methods is aspirational. ## Licence Code (the scripts) is MIT, see [LICENSE](LICENSE). The job data in `data/` is released under [CC0 1.0](https://creativecommons.org/publicdomain/zero/1.0/) — take it, mirror it, build on it. See [DATA-LICENSE.md](DATA-LICENSE.md).