面议

• / 安全
• 不限 / 本科

职位描述

**工作职责：** 1. 开发和维护用于智能合约等区块链代码的形式化验证引擎、工具链及生产流水线； 2. 分析智能合约等区块链样例代码的规范、模型、正确性、安全性并进行相应的形式化和证明； 3. 抽象、编写、维护智能合约等区块链常见代码模块、模板的通用形式化规范及证明脚本； 4. 分析、抽象形式化验证过程中的人工步骤及其自动化加速手段，开发和维护相应的工具及生产流水线； 5. 定义、观测、监控形式化验证应用过程中的质量、速度、效率等生产测度； 6. 分析、协同其它区块链安全工具和方法，提高区块链安全的总体质量，降低其总体成本； 7. 跨团队同审计师、软件开发工程师等进行合作，提升区块链形式化验证的实际效能。 **任职要求：** 1. 数理逻辑的经验和兴趣； 2. 自我驱动的学习动机和能力； 3. 善于文字和口头技术沟通； 4. 扎实的通用程序设计基础； 5. 程序分析调试的经验和兴趣； 6. 脚本工具的编写、使用经验； 7. C、C++、Java、Golang、Rust、Solidity等语言之一的实用编程经验； 8. 区块链软件栈的基础知识； 9. 熟悉Linux及GitHub的使用。 **优先考虑：** 1. 形式逻辑、形式化验证、定理证明、自动化验证等经验； 2. 程序或安全分析工具的使用和开发经验； 3. 区块链的深入知识和经验； 4. 智能合约编程或安全分析经验。

工作职责：

1. 开发和维护用于智能合约等区块链代码的形式化验证引擎、工具链及生产流水线；

2. 分析智能合约等区块链样例代码的规范、模型、正确性、安全性并进行相应的形式化和证明；

3. 抽象、编写、维护智能合约等区块链常见代码模块、模板的通用形式化规范及证明脚本；

4. 分析、抽象形式化验证过程中的人工步骤及其自动化加速手段，开发和维护相应的工具及生产流水线；

5. 定义、观测、监控形式化验证应用过程中的质量、速度、效率等生产测度；

6. 分析、协同其它区块链安全工具和方法，提高区块链安全的总体质量，降低其总体成本；

7. 跨团队同审计师、软件开发工程师等进行合作，提升区块链形式化验证的实际效能。

任职要求：

1. 数理逻辑的经验和兴趣；

2. 自我驱动的学习动机和能力；

3. 善于文字和口头技术沟通；

4. 扎实的通用程序设计基础；

5. 程序分析调试的经验和兴趣；

6. 脚本工具的编写、使用经验；

7. C、C++、Java、Golang、Rust、Solidity等语言之一的实用编程经验；

8. 区块链软件栈的基础知识；

9. 熟悉Linux及GitHub的使用。

优先考虑：

1. 形式逻辑、形式化验证、定理证明、自动化验证等经验；

2. 程序或安全分析工具的使用和开发经验；

3. 区块链的深入知识和经验；

4. 智能合约编程或安全分析经验。

工作地点

项目简介

CertiK是全球领先的Web3安全公司，总部位于美国纽约。CertiK为Web3行业提供全周期产品和服务，产品链跨越从初创、成长到扩张、成熟的全生命周期，支持Web3企业和生态的长期发展战略。 投递方式： 有意向者请将简历发送至[lian.tang@certik.com]，邮件主题注明“平台 - [岗位名称] - [应聘者姓名]”。

• 发布于 1天前
• 阅读 ( 32 )

免责声明

在登链社区网站、登链社区公众号及关联平台发布的招聘信息均系招聘方自行发布，登链社区只负责展示或格式编辑，对其招聘内容的合法性和真实性不承担任何法律责任，请求职者提高警惕，注意甄别！