一般信息
Runtime Verification是一种计算系统分析和执行的方法，旨在从运行中的系统中提取信息，以检测和可能响应观察到的行为是否满足或违反某些属性。这种技术可以用于多种目的，如安全或安全策略监控、调试、测试、验证、验证、性能分析、故障保护、行为修改等。它通过分析少量执行轨迹并直接与实际系统工作，避免了传统形式验证技术的复杂性。
Runtime Verification Inc.是一家专注于使用运行时验证技术进行虚拟机和智能合约安全审计的公司。他们提供的服务包括设计审查、代码审查、审计和智能合约及协议的形式验证。
Runtime Verification Inc. 目前提供哪些产品？
Runtime Verification Inc. 目前正在开发三个核心产品：RV-Predict 是一种预测性运行时分析工具，专注于自动检测程序中的并发错误。RV-Monitor 是一种开发方法和库生成工具，允许在运行时监控和执行用户选择的属性。RV-Match 是一种工具，允许对所有可能的程序路径以符号方式执行详尽的运行时验证，从而证明某些属性对于给定程序的所有可能执行都是正确的。
何时以及为何应使用 RV-Predict？
每当并发正确性对多线程应用程序很重要时，都应该使用 RV-Predict。RV-Predict 能够高效、无缝地检测程序中的并发问题和数据争用，非常易于运行，并且通常不需要任何配置。RV-Predict 还利用独特的预测功能来检测可能的争用，即使它们未发生在 RV-Predict 记录的执行跟踪中。
何时以及为何应使用 RV-Monitor？
RV-Monitor 允许监控复杂的应用程序或系统，并对其执行跟踪执行属性。只要存在用于管理程序开发的规范，就应使用 RV-Monitor，并且遵守该规范是软件的关键功能。RV-Monitor 还可用于监控对通用 API（包括 Android 和 Java API）的合规性。
何时以及为何应使用 RV-Match？
RV-Monitor 可以验证并强制符合给定程序执行的某些属性，而 RV-Match 可以在运行时证明程序的正确性，从而分析所有可能的执行路径和所有可能的输入上的执行跟踪。RV-Match 提供强大的正确性保证，利用目标语言的正式定义语义以符号方式模拟执行。当需要形式验证的有力保证时，应使用 RV-Match，也可以与 RV-Monitor 一起使用，以消除可证明从未违反属性的区域的监控。
Runtime Verification Inc. 的产品涵盖哪些许可证？
RV 开发的项目分为两类：专有产品和根据开放许可证许可的项目（作为 RV 开源生态系统的一部分）。
专有产品包括未根据开放许可证明确许可的所有产品，仅用于评估和学术/非商业目的。未经事先许可，不得使用专有 RV 产品创建衍生作品，并且 RV 保留对专有产品的所有权利。不得以任何方式对专有产品进行逆向工程。
区块链项目审计
Runtime Verification已经参与了多个区块链项目的审计工作，包括但不限于以下方面：
- 智能合约的安全审计：他们提供对ERC-20、ERC-721、ERC-4626等合约的低成本审计。
- 协议的安全审计：包括借贷相关操作的协议。
- 形式验证：提供开源的形式验证和开发者工具，以降低审计成本并实现持续的形式验证。
他们的审计通常包括手动审查和形式验证，确保代码的高安全性和可靠性。
