commit - 2c5d02a163216364610dc6cb30c23ec0eb17ce94
commit + d941858f9c1a1be16de495047a9150a1d3da215f
blob - ede6dbdb45ef872982576b762fa66324281c0dcf
blob + cba5461424ba4778a4f9be3b938b0a0f885675fc
--- README.md
+++ README.md
@@ -53,6 +53,7 @@ NASA | USA | Space | ```PVS``` [NASA Langley Formal Me
 [Oracle](https://www.oracle.com/) | Redwood Shores, CA, USA | Enterprise software, Cloud computing, Computer hardware | `ACL2` ([Proving Theorems about Java and the JVM with ACL2](https://www.cs.utexas.edu/users/moore/publications/marktoberdorf-02/index.html))
 [Particular Software](https://particular.net/) | | | ```TLA+``` [TLA+ Specifications for NServiceBus](https://github.com/tmasternak/NServiceBus.ModelChecking)
 PingCAP | | | ```TLA+``` [TLA+ in TiDB](https://github.com/pingcap/tla-plus)
+[Rusbitech](https://rusbitech.ru/) (РусБиТех) | Russia, Moscow | Системное ПО | `Frama-C`, `Event-B` ([Моделирование и верификация политик безопасности управления доступом в операционных системах](https://www.ispras.ru/publications/2018/security_policy_modeling_and_verification/)) |
 [Rockwell Collins](https://www.rockwellcollins.com/) | USA, Cedar Rapids, Iowa | High Assurance Systems | [Formal Methods in the Aerospace Industry: Follow the Money](http://www.jaist.ac.jp/icfem2012/Cofer-ICFEM2012.pdf)
 [Serokell](https://serokell.io/#tech) | Tallinn, Estonia | Fintech, blockchain, IoT, machine learning, formal verification | `Agda`
 [Synopsis](https://www.synopsys.com/) | ? | ? | [Site](https://www.synopsys.com/verification.html)